transgeo.miz



    begin

    reserve A for non empty set,

a,b,x,y,z,t for Element of A,

f,g,h for Permutation of A;

    definition

      let A be set, f,g be Permutation of A;

      :: original: *

      redefine

      func g * f -> Permutation of A ;

      coherence

      proof

        thus (g * f) is Permutation of A;

      end;

    end

    theorem :: TRANSGEO:1

    

     Th1: ex x st (f . x) = y

    proof

      ( rng f) = A by FUNCT_2:def 3;

      then ex x be object st x in ( dom f) & (f . x) = y by FUNCT_1:def 3;

      hence thesis;

    end;

    theorem :: TRANSGEO:2

    

     Th2: (f . x) = y iff ((f " ) . y) = x

    proof

       A1:

      now

        x in A;

        then

         A2: x in ( dom f) by FUNCT_2:def 1;

        assume (f . x) = y;

        hence x = ((f " ) . y) by A2, FUNCT_1: 34;

      end;

      ( rng f) = A by FUNCT_2:def 3;

      hence thesis by A1, FUNCT_1: 35;

    end;

    definition

      let A, f, g;

      :: TRANSGEO:def1

      func f \ g -> Permutation of A equals ((g * f) * (g " ));

      coherence ;

    end

    scheme :: TRANSGEO:sch1

    EXPermutation { A() -> non empty set , P[ object, object] } :

ex f be Permutation of A() st for x,y be Element of A() holds (f . x) = y iff P[x, y]

      provided

       A1: for x be Element of A() holds ex y be Element of A() st P[x, y]

       and

       A2: for y be Element of A() holds ex x be Element of A() st P[x, y]

       and

       A3: for x,y,x9 be Element of A() st P[x, y] & P[x9, y] holds x = x9

       and

       A4: for x,y,y9 be Element of A() st P[x, y] & P[x, y9] holds y = y9;

      

       A5: for x be Element of A() holds ex y be Element of A() st P[x, y] by A1;

      consider f be Function of A(), A() such that

       A6: for x be Element of A() holds P[x, (f . x)] from FUNCT_2:sch 3( A5);

      now

        let y be object;

        assume

         A7: y in A();

        then

        consider x be Element of A() such that

         A8: P[x, y] by A2;

        P[x, (f . x)] by A6;

        then (f . x) = y by A4, A7, A8;

        hence y in ( rng f) by FUNCT_2: 4;

      end;

      then A() c= ( rng f) by TARSKI:def 3;

      then

       A9: ( rng f) = A() by XBOOLE_0:def 10;

      now

        let x1,x2 be object;

        assume that

         A10: x1 in A() and

         A11: x2 in A();

        

         A12: (f . x1) is Element of A() by A10, FUNCT_2: 5;

        P[x1, (f . x1)] & P[x2, (f . x2)] by A6, A10, A11;

        hence (f . x1) = (f . x2) implies x1 = x2 by A3, A10, A11, A12;

      end;

      then f is one-to-one by FUNCT_2: 19;

      then

      reconsider f as Permutation of A() by A9, FUNCT_2: 57;

      take f;

      let x,y be Element of A();

      thus (f . x) = y implies P[x, y] by A6;

      assume

       A13: P[x, y];

      P[x, (f . x)] by A6;

      hence thesis by A4, A13;

    end;

    theorem :: TRANSGEO:3

    (f . ((f " ) . x)) = x & ((f " ) . (f . x)) = x by Th2;

    theorem :: TRANSGEO:4

    (f * ( id A)) = (( id A) * f)

    proof

      (f * ( id A)) = f by FUNCT_2: 17;

      hence thesis by FUNCT_2: 17;

    end;

    

     Lm1: (f * g) = (f * h) implies g = h

    proof

      assume (f * g) = (f * h);

      then (((f " ) * f) * g) = ((f " ) * (f * h)) by RELAT_1: 36;

      then (((f " ) * f) * g) = (((f " ) * f) * h) by RELAT_1: 36;

      then (( id A) * g) = (((f " ) * f) * h) by FUNCT_2: 61;

      then (( id A) * g) = (( id A) * h) by FUNCT_2: 61;

      then g = (( id A) * h) by FUNCT_2: 17;

      hence thesis by FUNCT_2: 17;

    end;

    

     Lm2: (g * f) = (h * f) implies g = h

    proof

      assume (g * f) = (h * f);

      then (g * (f * (f " ))) = ((h * f) * (f " )) by RELAT_1: 36;

      then (g * (f * (f " ))) = (h * (f * (f " ))) by RELAT_1: 36;

      then (g * ( id A)) = (h * (f * (f " ))) by FUNCT_2: 61;

      then (g * ( id A)) = (h * ( id A)) by FUNCT_2: 61;

      then g = (h * ( id A)) by FUNCT_2: 17;

      hence thesis by FUNCT_2: 17;

    end;

    theorem :: TRANSGEO:5

    (g * f) = (h * f) or (f * g) = (f * h) implies g = h by Lm1, Lm2;

    theorem :: TRANSGEO:6

    ((f * g) \ h) = ((f \ h) * (g \ h))

    proof

      

      thus ((f * g) \ h) = ((h * (f * (( id A) * g))) * (h " )) by FUNCT_2: 17

      .= ((h * (f * (((h " ) * h) * g))) * (h " )) by FUNCT_2: 61

      .= ((h * (f * ((h " ) * (h * g)))) * (h " )) by RELAT_1: 36

      .= ((h * ((f * (h " )) * (h * g))) * (h " )) by RELAT_1: 36

      .= (((h * (f * (h " ))) * (h * g)) * (h " )) by RELAT_1: 36

      .= ((h * (f * (h " ))) * ((h * g) * (h " ))) by RELAT_1: 36

      .= ((f \ h) * (g \ h)) by RELAT_1: 36;

    end;

    theorem :: TRANSGEO:7

    ((f " ) \ g) = ((f \ g) " )

    proof

      

      thus ((f \ g) " ) = (((g " ) " ) * ((g * f) " )) by FUNCT_1: 44

      .= (((g " ) " ) * ((f " ) * (g " ))) by FUNCT_1: 44

      .= (g * ((f " ) * (g " ))) by FUNCT_1: 43

      .= ((f " ) \ g) by RELAT_1: 36;

    end;

    theorem :: TRANSGEO:8

    (f \ (g * h)) = ((f \ h) \ g)

    proof

      

      thus (f \ (g * h)) = (((g * h) * f) * ((h " ) * (g " ))) by FUNCT_1: 44

      .= ((((g * h) * f) * (h " )) * (g " )) by RELAT_1: 36

      .= (((g * (h * f)) * (h " )) * (g " )) by RELAT_1: 36

      .= ((f \ h) \ g) by RELAT_1: 36;

    end;

    theorem :: TRANSGEO:9

    (( id A) \ f) = ( id A)

    proof

      

      thus (( id A) \ f) = (f * (f " )) by FUNCT_2: 17

      .= ( id A) by FUNCT_2: 61;

    end;

    theorem :: TRANSGEO:10

    (f \ ( id A)) = f

    proof

      

      thus (f \ ( id A)) = (f * (( id A) " )) by FUNCT_2: 17

      .= (f * ( id A)) by FUNCT_1: 45

      .= f by FUNCT_2: 17;

    end;

    theorem :: TRANSGEO:11

    (f . a) = a implies ((f \ g) . (g . a)) = (g . a)

    proof

      assume

       A1: (f . a) = a;

      ((g " ) . (g . a)) = (((g " ) * g) . a) by FUNCT_2: 15

      .= (( id A) . a) by FUNCT_2: 61

      .= a;

      

      hence ((f \ g) . (g . a)) = ((g * f) . a) by FUNCT_2: 15

      .= (g . a) by A1, FUNCT_2: 15;

    end;

    reserve R for Relation of [:A, A:];

    definition

      let A, f, R;

      :: TRANSGEO:def2

      pred f is_FormalIz_of R means for x, y holds [ [x, y], [(f . x), (f . y)]] in R;

    end

    theorem :: TRANSGEO:12

    

     Th12: R is_reflexive_in [:A, A:] implies ( id A) is_FormalIz_of R

    proof

      assume

       A1: for x be object st x in [:A, A:] holds [x, x] in R;

      let x, y;

      

       A2: [x, y] in [:A, A:] by ZFMISC_1:def 2;

      thus thesis by A1, A2;

    end;

    theorem :: TRANSGEO:13

    

     Th13: R is_symmetric_in [:A, A:] & f is_FormalIz_of R implies (f " ) is_FormalIz_of R

    proof

      assume

       A1: for x,y be object st x in [:A, A:] & y in [:A, A:] & [x, y] in R holds [y, x] in R;

      assume

       A2: for x, y holds [ [x, y], [(f . x), (f . y)]] in R;

      let x, y;

      

       A3: [ [((f " ) . x), ((f " ) . y)], [(f . ((f " ) . x)), (f . ((f " ) . y))]] in R by A2;

      

       A4: [((f " ) . x), ((f " ) . y)] in [:A, A:] & [(f . ((f " ) . x)), (f . ((f " ) . y))] in [:A, A:] by ZFMISC_1:def 2;

      (f . ((f " ) . x)) = x & (f . ((f " ) . y)) = y by Th2;

      hence thesis by A1, A3, A4;

    end;

    theorem :: TRANSGEO:14

    R is_transitive_in [:A, A:] & f is_FormalIz_of R & g is_FormalIz_of R implies (f * g) is_FormalIz_of R

    proof

      assume that

       A1: for x,y,z be object st x in [:A, A:] & y in [:A, A:] & z in [:A, A:] & [x, y] in R & [y, z] in R holds [x, z] in R and

       A2: for x, y holds [ [x, y], [(f . x), (f . y)]] in R and

       A3: for x, y holds [ [x, y], [(g . x), (g . y)]] in R;

      let x, y;

      (f . (g . x)) = ((f * g) . x) & (f . (g . y)) = ((f * g) . y) by FUNCT_2: 15;

      then

       A4: [ [(g . x), (g . y)], [((f * g) . x), ((f * g) . y)]] in R by A2;

      

       A5: [((f * g) . x), ((f * g) . y)] in [:A, A:] by ZFMISC_1:def 2;

      

       A6: [x, y] in [:A, A:] & [(g . x), (g . y)] in [:A, A:] by ZFMISC_1:def 2;

       [ [x, y], [(g . x), (g . y)]] in R by A3;

      hence thesis by A1, A4, A6, A5;

    end;

    theorem :: TRANSGEO:15

    

     Th15: (for a, b, x, y, z, t st [ [x, y], [a, b]] in R & [ [a, b], [z, t]] in R & a <> b holds [ [x, y], [z, t]] in R) & (for x, y, z holds [ [x, x], [y, z]] in R) & f is_FormalIz_of R & g is_FormalIz_of R implies (f * g) is_FormalIz_of R

    proof

      assume that

       A1: for a, b, x, y, z, t st [ [x, y], [a, b]] in R & [ [a, b], [z, t]] in R & a <> b holds [ [x, y], [z, t]] in R and

       A2: for x, y, z holds [ [x, x], [y, z]] in R and

       A3: for x, y holds [ [x, y], [(f . x), (f . y)]] in R and

       A4: for x, y holds [ [x, y], [(g . x), (g . y)]] in R;

      let x, y;

      (f . (g . x)) = ((f * g) . x) & (f . (g . y)) = ((f * g) . y) by FUNCT_2: 15;

      then

       A5: [ [(g . x), (g . y)], [((f * g) . x), ((f * g) . y)]] in R by A3;

       A6:

      now

        assume (g . x) = (g . y);

        then x = y by FUNCT_2: 58;

        hence thesis by A2;

      end;

       [ [x, y], [(g . x), (g . y)]] in R by A4;

      hence thesis by A1, A5, A6;

    end;

    definition

      let A;

      let f;

      let R;

      :: TRANSGEO:def3

      pred f is_automorphism_of R means for x, y, z, t holds ( [ [x, y], [z, t]] in R iff [ [(f . x), (f . y)], [(f . z), (f . t)]] in R);

    end

    theorem :: TRANSGEO:16

    ( id A) is_automorphism_of R;

    theorem :: TRANSGEO:17

    

     Th17: f is_automorphism_of R implies (f " ) is_automorphism_of R

    proof

      assume

       A1: for x, y, z, t holds ( [ [x, y], [z, t]] in R iff [ [(f . x), (f . y)], [(f . z), (f . t)]] in R);

      let x, y, z, t;

      

       A2: (f . ((f " ) . z)) = z & (f . ((f " ) . t)) = t by Th2;

      (f . ((f " ) . x)) = x & (f . ((f " ) . y)) = y by Th2;

      hence thesis by A1, A2;

    end;

    theorem :: TRANSGEO:18

    

     Th18: f is_automorphism_of R & g is_automorphism_of R implies (g * f) is_automorphism_of R

    proof

      assume that

       A1: for x, y, z, t holds ( [ [x, y], [z, t]] in R iff [ [(f . x), (f . y)], [(f . z), (f . t)]] in R) and

       A2: for x, y, z, t holds ( [ [x, y], [z, t]] in R iff [ [(g . x), (g . y)], [(g . z), (g . t)]] in R);

      let x, y, z, t;

      

       A3: (g . (f . x)) = ((g * f) . x) & (g . (f . y)) = ((g * f) . y) by FUNCT_2: 15;

      

       A4: (g . (f . z)) = ((g * f) . z) & (g . (f . t)) = ((g * f) . t) by FUNCT_2: 15;

       [ [x, y], [z, t]] in R iff [ [(f . x), (f . y)], [(f . z), (f . t)]] in R by A1;

      hence thesis by A2, A3, A4;

    end;

    theorem :: TRANSGEO:19

    R is_symmetric_in [:A, A:] & R is_transitive_in [:A, A:] & f is_FormalIz_of R implies f is_automorphism_of R

    proof

      assume that

       A1: for x,y be object st x in [:A, A:] & y in [:A, A:] & [x, y] in R holds [y, x] in R and

       A2: for x,y,z be object st x in [:A, A:] & y in [:A, A:] & z in [:A, A:] & [x, y] in R & [y, z] in R holds [x, z] in R and

       A3: for x, y holds [ [x, y], [(f . x), (f . y)]] in R;

      let x, y, z, t;

      

       A4: [z, t] in [:A, A:] by ZFMISC_1:def 2;

      

       A5: [(f . z), (f . t)] in [:A, A:] by ZFMISC_1:def 2;

      

       A6: [(f . x), (f . y)] in [:A, A:] by ZFMISC_1:def 2;

      

       A7: [x, y] in [:A, A:] by ZFMISC_1:def 2;

       A8:

      now

         [ [z, t], [(f . z), (f . t)]] in R by A3;

        then

         A9: [ [(f . z), (f . t)], [z, t]] in R by A1, A4, A5;

        assume

         A10: [ [(f . x), (f . y)], [(f . z), (f . t)]] in R;

         [ [x, y], [(f . x), (f . y)]] in R by A3;

        then [ [x, y], [(f . z), (f . t)]] in R by A2, A7, A6, A5, A10;

        hence [ [x, y], [z, t]] in R by A2, A7, A4, A5, A9;

      end;

      now

         [ [x, y], [(f . x), (f . y)]] in R by A3;

        then

         A11: [ [(f . x), (f . y)], [x, y]] in R by A1, A7, A6;

        

         A12: [ [z, t], [(f . z), (f . t)]] in R by A3;

        assume [ [x, y], [z, t]] in R;

        then [ [(f . x), (f . y)], [z, t]] in R by A2, A7, A4, A6, A11;

        hence [ [(f . x), (f . y)], [(f . z), (f . t)]] in R by A2, A4, A6, A5, A12;

      end;

      hence thesis by A8;

    end;

    theorem :: TRANSGEO:20

    (for a, b, x, y, z, t st [ [x, y], [a, b]] in R & [ [a, b], [z, t]] in R & a <> b holds [ [x, y], [z, t]] in R) & (for x, y, z holds [ [x, x], [y, z]] in R) & R is_symmetric_in [:A, A:] & f is_FormalIz_of R implies f is_automorphism_of R

    proof

      assume that

       A1: for a, b, x, y, z, t st [ [x, y], [a, b]] in R & [ [a, b], [z, t]] in R & a <> b holds [ [x, y], [z, t]] in R and

       A2: for x, y, z holds [ [x, x], [y, z]] in R and

       A3: for x,y be object st x in [:A, A:] & y in [:A, A:] & [x, y] in R holds [y, x] in R and

       A4: for x, y holds [ [x, y], [(f . x), (f . y)]] in R;

      

       A5: for x, y, z holds [ [y, z], [x, x]] in R

      proof

        let x, y, z;

        

         A6: [y, z] in [:A, A:] & [x, x] in [:A, A:] by ZFMISC_1:def 2;

         [ [x, x], [y, z]] in R by A2;

        hence thesis by A3, A6;

      end;

      let x, y, z, t;

      

       A7: [ [x, y], [(f . x), (f . y)]] in R by A4;

      

       A8: [ [z, t], [(f . z), (f . t)]] in R by A4;

       [z, t] in [:A, A:] & [(f . z), (f . t)] in [:A, A:] by ZFMISC_1:def 2;

      then

       A9: [ [(f . z), (f . t)], [z, t]] in R by A3, A8;

       A10:

      now

        assume

         A11: [ [(f . x), (f . y)], [(f . z), (f . t)]] in R;

         A12:

        now

          assume that

           A13: (f . x) <> (f . y) and

           A14: (f . z) <> (f . t);

           [ [x, y], [(f . z), (f . t)]] in R by A1, A7, A11, A13;

          hence [ [x, y], [z, t]] in R by A1, A9, A14;

        end;

         A15:

        now

          assume (f . z) = (f . t);

          then z = t by FUNCT_2: 58;

          hence [ [x, y], [z, t]] in R by A5;

        end;

        now

          assume (f . x) = (f . y);

          then x = y by FUNCT_2: 58;

          hence [ [x, y], [z, t]] in R by A2;

        end;

        hence [ [x, y], [z, t]] in R by A15, A12;

      end;

       [x, y] in [:A, A:] & [(f . x), (f . y)] in [:A, A:] by ZFMISC_1:def 2;

      then

       A16: [ [(f . x), (f . y)], [x, y]] in R by A3, A7;

      now

        assume

         A17: [ [x, y], [z, t]] in R;

        now

          assume that

           A18: x <> y and

           A19: z <> t;

           [ [(f . x), (f . y)], [z, t]] in R by A1, A16, A17, A18;

          hence [ [(f . x), (f . y)], [(f . z), (f . t)]] in R by A1, A8, A19;

        end;

        hence [ [(f . x), (f . y)], [(f . z), (f . t)]] in R by A2, A5;

      end;

      hence thesis by A10;

    end;

    theorem :: TRANSGEO:21

    f is_FormalIz_of R & g is_automorphism_of R implies (f \ g) is_FormalIz_of R

    proof

      assume that

       A1: for x, y holds [ [x, y], [(f . x), (f . y)]] in R and

       A2: for x, y, z, t holds ( [ [x, y], [z, t]] in R iff [ [(g . x), (g . y)], [(g . z), (g . t)]] in R);

      let x, y;

      

       A3: [ [((g " ) . x), ((g " ) . y)], [(f . ((g " ) . x)), (f . ((g " ) . y))]] in R by A1;

      (g . ((g " ) . x)) = x & (g . ((g " ) . y)) = y by Th2;

      then [ [x, y], [(g . (f . ((g " ) . x))), (g . (f . ((g " ) . y)))]] in R by A2, A3;

      then [ [x, y], [((g * f) . ((g " ) . x)), (g . (f . ((g " ) . y)))]] in R by FUNCT_2: 15;

      then [ [x, y], [((g * f) . ((g " ) . x)), ((g * f) . ((g " ) . y))]] in R by FUNCT_2: 15;

      then [ [x, y], [(((g * f) * (g " )) . x), ((g * f) . ((g " ) . y))]] in R by FUNCT_2: 15;

      hence thesis by FUNCT_2: 15;

    end;

    reserve AS for non empty AffinStruct;

    definition

      let AS;

      let f be Permutation of the carrier of AS;

      :: TRANSGEO:def4

      pred f is_DIL_of AS means f is_FormalIz_of the CONGR of AS;

    end

    reserve a,b,x,y for Element of AS;

    theorem :: TRANSGEO:22

    

     Th22: for f be Permutation of the carrier of AS holds (f is_DIL_of AS iff for a, b holds (a,b) // ((f . a),(f . b)))

    proof

      let f be Permutation of the carrier of AS;

       A1:

      now

        assume

         A2: for a, b holds (a,b) // ((f . a),(f . b));

        for x, y holds [ [x, y], [(f . x), (f . y)]] in the CONGR of AS by A2, ANALOAF:def 2;

        then f is_FormalIz_of the CONGR of AS;

        hence f is_DIL_of AS;

      end;

      now

        assume

         A3: f is_DIL_of AS;

        let a, b;

        f is_FormalIz_of the CONGR of AS by A3;

        then [ [a, b], [(f . a), (f . b)]] in the CONGR of AS;

        hence (a,b) // ((f . a),(f . b)) by ANALOAF:def 2;

      end;

      hence thesis by A1;

    end;

    definition

      let IT be non empty AffinStruct;

      :: TRANSGEO:def5

      attr IT is CongrSpace-like means

      : Def5: (for x,y,z,t,a,b be Element of IT st (x,y) // (a,b) & (a,b) // (z,t) & a <> b holds (x,y) // (z,t)) & (for x,y,z be Element of IT holds (x,x) // (y,z)) & (for x,y,z,t be Element of IT st (x,y) // (z,t) holds (z,t) // (x,y)) & for x,y be Element of IT holds (x,y) // (x,y);

    end

    registration

      cluster strict CongrSpace-like for non empty AffinStruct;

      existence

      proof

        set OAS = the strict OAffinSpace;

        

         A1: (for x,y,z,t be Element of OAS st (x,y) // (z,t) holds (z,t) // (x,y)) & for x,y be Element of OAS holds (x,y) // (x,y) by DIRAF: 1, DIRAF: 2;

        (for x,y,z,t,a,b be Element of OAS st (x,y) // (a,b) & (a,b) // (z,t) & a <> b holds (x,y) // (z,t)) & for x,y,z be Element of OAS holds (x,x) // (y,z) by DIRAF: 3, DIRAF: 4;

        then OAS is CongrSpace-like by A1;

        hence thesis;

      end;

    end

    definition

      mode CongrSpace is CongrSpace-like non empty AffinStruct;

    end

    reserve CS for CongrSpace;

    

     Lm3: the CONGR of CS is_reflexive_in [:the carrier of CS, the carrier of CS:]

    proof

      let x be object;

      assume x in [:the carrier of CS, the carrier of CS:];

      then

      consider x1,x2 be Element of CS such that

       A1: x = [x1, x2] by DOMAIN_1: 1;

      (x1,x2) // (x1,x2) by Def5;

      hence thesis by A1, ANALOAF:def 2;

    end;

    

     Lm4: the CONGR of CS is_symmetric_in [:the carrier of CS, the carrier of CS:]

    proof

      let x,y be object;

      assume that

       A1: x in [:the carrier of CS, the carrier of CS:] and

       A2: y in [:the carrier of CS, the carrier of CS:] and

       A3: [x, y] in the CONGR of CS;

      consider x1,x2 be Element of CS such that

       A4: x = [x1, x2] by A1, DOMAIN_1: 1;

      consider y1,y2 be Element of CS such that

       A5: y = [y1, y2] by A2, DOMAIN_1: 1;

      (x1,x2) // (y1,y2) by A3, A4, A5, ANALOAF:def 2;

      then (y1,y2) // (x1,x2) by Def5;

      hence thesis by A4, A5, ANALOAF:def 2;

    end;

    theorem :: TRANSGEO:23

    

     Th23: ( id the carrier of CS) is_DIL_of CS by Lm3, Th12;

    theorem :: TRANSGEO:24

    

     Th24: for f be Permutation of the carrier of CS st f is_DIL_of CS holds (f " ) is_DIL_of CS by Lm4, Th13;

    theorem :: TRANSGEO:25

    

     Th25: for f,g be Permutation of the carrier of CS st f is_DIL_of CS & g is_DIL_of CS holds (f * g) is_DIL_of CS

    proof

      let f,g be Permutation of the carrier of CS;

       A1:

      now

        let a,b,x,y,z,t be Element of CS;

        assume that

         A2: [ [x, y], [a, b]] in the CONGR of CS & [ [a, b], [z, t]] in the CONGR of CS and

         A3: a <> b;

        (x,y) // (a,b) & (a,b) // (z,t) by A2, ANALOAF:def 2;

        then (x,y) // (z,t) by A3, Def5;

        hence [ [x, y], [z, t]] in the CONGR of CS by ANALOAF:def 2;

      end;

       A4:

      now

        let x,y,z be Element of CS;

        (x,x) // (y,z) by Def5;

        hence [ [x, x], [y, z]] in the CONGR of CS by ANALOAF:def 2;

      end;

      assume f is_DIL_of CS & g is_DIL_of CS;

      then f is_FormalIz_of the CONGR of CS & g is_FormalIz_of the CONGR of CS;

      then (f * g) is_FormalIz_of the CONGR of CS by A1, A4, Th15;

      hence thesis;

    end;

    reserve OAS for OAffinSpace;

    reserve a,b,c,d,p,q,r,x,y,z,t,u for Element of OAS;

    theorem :: TRANSGEO:26

    

     Th26: OAS is CongrSpace-like by DIRAF: 3, DIRAF: 4, DIRAF: 2, DIRAF: 1;

    reserve f,g for Permutation of the carrier of OAS;

    definition

      let OAS;

      let f be Permutation of the carrier of OAS;

      :: TRANSGEO:def6

      attr f is positive_dilatation means f is_DIL_of OAS;

    end

    theorem :: TRANSGEO:27

    

     Th27: for f be Permutation of the carrier of OAS holds (f is positive_dilatation iff for a, b holds (a,b) // ((f . a),(f . b))) by Th22;

    definition

      let OAS;

      let f be Permutation of the carrier of OAS;

      :: TRANSGEO:def7

      attr f is negative_dilatation means for a, b holds (a,b) // ((f . b),(f . a));

    end

    theorem :: TRANSGEO:28

    

     Th28: ( id the carrier of OAS) is positive_dilatation

    proof

      OAS is CongrSpace by Th26;

      then ( id the carrier of OAS) is_DIL_of OAS by Th23;

      hence thesis;

    end;

    theorem :: TRANSGEO:29

    for f be Permutation of the carrier of OAS st f is positive_dilatation holds (f " ) is positive_dilatation

    proof

      let f be Permutation of the carrier of OAS;

      assume f is positive_dilatation;

      then

       A1: f is_DIL_of OAS;

      OAS is CongrSpace by Th26;

      then (f " ) is_DIL_of OAS by A1, Th24;

      hence thesis;

    end;

    theorem :: TRANSGEO:30

    for f,g be Permutation of the carrier of OAS st f is positive_dilatation & g is positive_dilatation holds (f * g) is positive_dilatation

    proof

      let f,g be Permutation of the carrier of OAS;

      assume f is positive_dilatation & g is positive_dilatation;

      then

       A1: f is_DIL_of OAS & g is_DIL_of OAS;

      OAS is CongrSpace by Th26;

      then (f * g) is_DIL_of OAS by A1, Th25;

      hence thesis;

    end;

    theorem :: TRANSGEO:31

     not ex f st f is negative_dilatation & f is positive_dilatation

    proof

      given f such that

       A1: f is negative_dilatation & f is positive_dilatation;

      consider a, b such that

       A2: a <> b by STRUCT_0:def 10;

      (a,b) // ((f . a),(f . b)) & (a,b) // ((f . b),(f . a)) by A1, Th27;

      then ((f . a),(f . b)) // ((f . b),(f . a)) by A2, ANALOAF:def 5;

      then (f . a) = (f . b) by ANALOAF:def 5;

      hence contradiction by A2, FUNCT_2: 58;

    end;

    theorem :: TRANSGEO:32

    f is negative_dilatation implies (f " ) is negative_dilatation

    proof

      assume

       A1: f is negative_dilatation;

      let x, y;

      set x9 = ((f " ) . x), y9 = ((f " ) . y);

      (f . x9) = x & (f . y9) = y by Th2;

      then (y9,x9) // (x,y) by A1;

      hence thesis by DIRAF: 2;

    end;

    theorem :: TRANSGEO:33

    f is positive_dilatation & g is negative_dilatation implies (f * g) is negative_dilatation & (g * f) is negative_dilatation

    proof

      assume

       A1: f is positive_dilatation & g is negative_dilatation;

      thus (x,y) // (((f * g) . y),((f * g) . x))

      proof

        set x9 = (g . x);

        set y9 = (g . y);

        

         A2: ((f * g) . x) = (f . x9) & ((f * g) . y) = (f . y9) by FUNCT_2: 15;

         A3:

        now

          assume x9 = y9;

          then x = y by FUNCT_2: 58;

          hence thesis by DIRAF: 4;

        end;

        (x,y) // (y9,x9) & (y9,x9) // ((f . y9),(f . x9)) by A1, Th27;

        hence thesis by A2, A3, DIRAF: 3;

      end;

      thus (x,y) // (((g * f) . y),((g * f) . x))

      proof

        set x9 = (f . x);

        set y9 = (f . y);

        

         A4: ((g * f) . x) = (g . x9) & ((g * f) . y) = (g . y9) by FUNCT_2: 15;

         A5:

        now

          assume x9 = y9;

          then x = y by FUNCT_2: 58;

          hence thesis by DIRAF: 4;

        end;

        (x,y) // (x9,y9) & (x9,y9) // ((g . y9),(g . x9)) by A1, Th27;

        hence thesis by A4, A5, DIRAF: 3;

      end;

    end;

    definition

      let OAS;

      let f be Permutation of the carrier of OAS;

      :: TRANSGEO:def8

      attr f is dilatation means f is_FormalIz_of ( lambda the CONGR of OAS);

    end

    theorem :: TRANSGEO:34

    

     Th34: for f be Permutation of the carrier of OAS holds (f is dilatation iff for a, b holds (a,b) '||' ((f . a),(f . b)))

    proof

      let f be Permutation of the carrier of OAS;

       A1:

      now

        assume

         A2: for a, b holds (a,b) '||' ((f . a),(f . b));

        for a, b holds [ [a, b], [(f . a), (f . b)]] in ( lambda the CONGR of OAS) by A2, DIRAF: 18;

        then f is_FormalIz_of ( lambda the CONGR of OAS);

        hence f is dilatation;

      end;

      now

        assume

         A3: f is dilatation;

        let a, b;

        f is_FormalIz_of ( lambda the CONGR of OAS) by A3;

        then [ [a, b], [(f . a), (f . b)]] in ( lambda the CONGR of OAS);

        hence (a,b) '||' ((f . a),(f . b)) by DIRAF: 18;

      end;

      hence thesis by A1;

    end;

    theorem :: TRANSGEO:35

    f is positive_dilatation or f is negative_dilatation implies f is dilatation

    proof

      assume

       A1: f is positive_dilatation or f is negative_dilatation;

      now

        let x, y;

        (x,y) // ((f . x),(f . y)) or (x,y) // ((f . y),(f . x)) by A1, Th27;

        hence (x,y) '||' ((f . x),(f . y)) by DIRAF:def 4;

      end;

      hence thesis by Th34;

    end;

    theorem :: TRANSGEO:36

    for f be Permutation of the carrier of OAS st f is dilatation holds ex f9 be Permutation of the carrier of ( Lambda OAS) st f = f9 & f9 is_DIL_of ( Lambda OAS)

    proof

      let f be Permutation of the carrier of OAS;

      

       A1: ( Lambda OAS) = AffinStruct (# the carrier of OAS, ( lambda the CONGR of OAS) #) by DIRAF:def 2;

      then

      reconsider f9 = f as Permutation of the carrier of ( Lambda OAS);

      assume f is dilatation;

      then

       A2: f is_FormalIz_of ( lambda the CONGR of OAS);

      take f9;

      thus thesis by A2, A1;

    end;

    theorem :: TRANSGEO:37

    for f be Permutation of the carrier of ( Lambda OAS) st f is_DIL_of ( Lambda OAS) holds ex f9 be Permutation of the carrier of OAS st f = f9 & f9 is dilatation

    proof

      let f be Permutation of the carrier of ( Lambda OAS);

      

       A1: ( Lambda OAS) = AffinStruct (# the carrier of OAS, ( lambda the CONGR of OAS) #) by DIRAF:def 2;

      then

      reconsider f9 = f as Permutation of the carrier of OAS;

      assume f is_DIL_of ( Lambda OAS);

      then

       A2: f is_FormalIz_of the CONGR of ( Lambda OAS);

      take f9;

      thus thesis by A2, A1;

    end;

    theorem :: TRANSGEO:38

    ( id the carrier of OAS) is dilatation

    proof

      for x, y holds (x,y) '||' ((( id the carrier of OAS) . x),(( id the carrier of OAS) . y)) by DIRAF: 19;

      hence thesis by Th34;

    end;

    theorem :: TRANSGEO:39

    f is positive_dilatation or f is negative_dilatation implies f is dilatation

    proof

      assume

       A1: f is positive_dilatation or f is negative_dilatation;

      now

        let x, y;

        (x,y) // ((f . x),(f . y)) or (x,y) // ((f . y),(f . x)) by A1, Th27;

        hence (x,y) '||' ((f . x),(f . y)) by DIRAF:def 4;

      end;

      hence thesis by Th34;

    end;

    theorem :: TRANSGEO:40

    for f be Permutation of the carrier of OAS st f is dilatation holds ex f9 be Permutation of the carrier of ( Lambda OAS) st f = f9 & f9 is_DIL_of ( Lambda OAS)

    proof

      let f be Permutation of the carrier of OAS;

      

       A1: ( Lambda OAS) = AffinStruct (# the carrier of OAS, ( lambda the CONGR of OAS) #) by DIRAF:def 2;

      then

      reconsider f9 = f as Permutation of the carrier of ( Lambda OAS);

      assume f is dilatation;

      then

       A2: f is_FormalIz_of ( lambda the CONGR of OAS);

      take f9;

      thus thesis by A2, A1;

    end;

    theorem :: TRANSGEO:41

    for f be Permutation of the carrier of ( Lambda OAS) st f is_DIL_of ( Lambda OAS) holds ex f9 be Permutation of the carrier of OAS st f = f9 & f9 is dilatation

    proof

      let f be Permutation of the carrier of ( Lambda OAS);

      

       A1: ( Lambda OAS) = AffinStruct (# the carrier of OAS, ( lambda the CONGR of OAS) #) by DIRAF:def 2;

      then

      reconsider f9 = f as Permutation of the carrier of OAS;

      assume f is_DIL_of ( Lambda OAS);

      then

       A2: f is_FormalIz_of the CONGR of ( Lambda OAS);

      take f9;

      thus thesis by A2, A1;

    end;

    theorem :: TRANSGEO:42

    ( id the carrier of OAS) is dilatation

    proof

      for x, y holds (x,y) '||' ((( id the carrier of OAS) . x),(( id the carrier of OAS) . y)) by DIRAF: 19;

      hence thesis by Th34;

    end;

    theorem :: TRANSGEO:43

    

     Th43: f is dilatation implies (f " ) is dilatation

    proof

      assume

       A1: f is dilatation;

      now

        let x, y;

        set x9 = ((f " ) . x);

        set y9 = ((f " ) . y);

        (f . x9) = x & (f . y9) = y by Th2;

        then (x9,y9) '||' (x,y) by A1, Th34;

        hence (x,y) '||' (((f " ) . x),((f " ) . y)) by DIRAF: 22;

      end;

      hence thesis by Th34;

    end;

    theorem :: TRANSGEO:44

    

     Th44: f is dilatation & g is dilatation implies (f * g) is dilatation

    proof

      assume

       A1: f is dilatation & g is dilatation;

      now

        let x, y;

        set x9 = (g . x);

        set y9 = (g . y);

        

         A2: ((f * g) . x) = (f . x9) & ((f * g) . y) = (f . y9) by FUNCT_2: 15;

         A3:

        now

          assume x9 = y9;

          then x = y by FUNCT_2: 58;

          hence (x,y) '||' (((f * g) . x),((f * g) . y)) by DIRAF: 20;

        end;

        (x,y) '||' (x9,y9) & (x9,y9) '||' ((f . x9),(f . y9)) by A1, Th34;

        hence (x,y) '||' (((f * g) . x),((f * g) . y)) by A2, A3, DIRAF: 23;

      end;

      hence thesis by Th34;

    end;

    theorem :: TRANSGEO:45

    

     Th45: f is dilatation implies for a, b, c, d holds (a,b) '||' (c,d) iff ((f . a),(f . b)) '||' ((f . c),(f . d))

    proof

      assume

       A1: f is dilatation;

      let a, b, c, d;

      

       A2: (c,d) '||' ((f . c),(f . d)) by A1, Th34;

      

       A3: (a,b) '||' ((f . a),(f . b)) by A1, Th34;

       A4:

      now

         A5:

        now

           A6:

          now

            assume (f . c) = (f . d);

            then c = d by FUNCT_2: 58;

            hence (a,b) '||' (c,d) by DIRAF: 20;

          end;

          assume (a,b) '||' ((f . c),(f . d));

          hence (a,b) '||' (c,d) by A2, A6, DIRAF: 23;

        end;

         A7:

        now

          assume (f . a) = (f . b);

          then a = b by FUNCT_2: 58;

          hence (a,b) '||' (c,d) by DIRAF: 20;

        end;

        assume ((f . a),(f . b)) '||' ((f . c),(f . d));

        hence (a,b) '||' (c,d) by A3, A7, A5, DIRAF: 23;

      end;

      now

         A8:

        now

          

           A9: c = d implies ((f . a),(f . b)) '||' ((f . c),(f . d)) by DIRAF: 20;

          assume ((f . a),(f . b)) '||' (c,d);

          hence ((f . a),(f . b)) '||' ((f . c),(f . d)) by A2, A9, DIRAF: 23;

        end;

        assume (a,b) '||' (c,d);

        then ((f . a),(f . b)) '||' (c,d) or a = b by A3, DIRAF: 23;

        hence ((f . a),(f . b)) '||' ((f . c),(f . d)) by A8, DIRAF: 20;

      end;

      hence thesis by A4;

    end;

    theorem :: TRANSGEO:46

    

     Th46: f is dilatation implies for a, b, c holds (a,b,c) are_collinear iff ((f . a),(f . b),(f . c)) are_collinear

    proof

      assume

       A1: f is dilatation;

      let a, b, c;

      (a,b) '||' (a,c) iff ((f . a),(f . b)) '||' ((f . a),(f . c)) by A1, Th45;

      hence thesis by DIRAF:def 5;

    end;

    theorem :: TRANSGEO:47

    

     Th47: f is dilatation & (x,(f . x),y) are_collinear implies (x,(f . x),(f . y)) are_collinear

    proof

      assume

       A1: f is dilatation;

      assume

       A2: (x,(f . x),y) are_collinear ;

      now

        assume

         A3: x <> y;

        (x,(f . x)) '||' (x,y) & (x,y) '||' ((f . x),(f . y)) by A1, A2, Th34, DIRAF:def 5;

        then (x,(f . x)) '||' ((f . x),(f . y)) by A3, DIRAF: 23;

        then ((f . x),x) '||' ((f . x),(f . y)) by DIRAF: 22;

        then ((f . x),x,(f . y)) are_collinear by DIRAF:def 5;

        hence thesis by DIRAF: 30;

      end;

      hence thesis by DIRAF: 31;

    end;

    theorem :: TRANSGEO:48

    

     Th48: (a,b) '||' (c,d) implies ((a,c) '||' (b,d) or ex x st (a,c,x) are_collinear & (b,d,x) are_collinear )

    proof

      assume

       A1: (a,b) '||' (c,d);

      assume

       A2: not (a,c) '||' (b,d);

       A3:

      now

        consider z such that

         A4: (a,b) '||' (c,z) and

         A5: (a,c) '||' (b,z) by DIRAF: 26;

        assume

         A6: a <> b;

         A7:

        now

          (c,d) '||' (c,z) by A1, A6, A4, DIRAF: 23;

          then (c,d,z) are_collinear by DIRAF:def 5;

          then (d,c,z) are_collinear by DIRAF: 30;

          then (d,c) '||' (d,z) by DIRAF:def 5;

          then (z,d) '||' (d,c) by DIRAF: 22;

          then

          consider t such that

           A8: (b,d) '||' (d,t) and

           A9: (b,z) '||' (c,t) by A2, A5, DIRAF: 27;

          assume b <> z;

          then (a,c) '||' (c,t) by A5, A9, DIRAF: 23;

          then (c,a) '||' (c,t) by DIRAF: 22;

          then (c,a,t) are_collinear by DIRAF:def 5;

          then

           A10: (a,c,t) are_collinear by DIRAF: 30;

          (d,b) '||' (d,t) by A8, DIRAF: 22;

          then (d,b,t) are_collinear by DIRAF:def 5;

          then (b,d,t) are_collinear by DIRAF: 30;

          hence thesis by A10;

        end;

        now

          assume b = z;

          then (b,a) '||' (b,c) by A4, DIRAF: 22;

          then (b,a,c) are_collinear by DIRAF:def 5;

          then

           A11: (a,c,b) are_collinear by DIRAF: 30;

          (b,d,b) are_collinear by DIRAF: 31;

          hence thesis by A11;

        end;

        hence thesis by A7;

      end;

      now

        assume a = b;

        then (a,c,a) are_collinear & (b,d,a) are_collinear by DIRAF: 31;

        hence thesis;

      end;

      hence thesis by A3;

    end;

    theorem :: TRANSGEO:49

    

     Th49: f is dilatation implies ((f = ( id the carrier of OAS) or for x holds (f . x) <> x) iff for x, y holds (x,(f . x)) '||' (y,(f . y)))

    proof

      assume

       A1: f is dilatation;

       A2:

      now

        assume

         A3: for x, y holds (x,(f . x)) '||' (y,(f . y));

        assume f <> ( id the carrier of OAS);

        then

        consider y such that

         A4: (f . y) <> (( id the carrier of OAS) . y) by FUNCT_2: 63;

        given x such that

         A5: (f . x) = x;

        x <> y by A5, A4;

        then

        consider z such that

         A6: not (x,y,z) are_collinear by DIRAF: 37;

        (x,z) '||' ((f . x),(f . z)) by A1, Th34;

        then (x,z,(f . z)) are_collinear by A5, DIRAF:def 5;

        then

         A7: (z,(f . z),x) are_collinear by DIRAF: 30;

        (z,(f . z),z) are_collinear by DIRAF: 31;

        then

         A8: (z,(f . z)) '||' (x,z) by A7, DIRAF: 34;

        

         A9: (f . y) <> y by A4;

        (x,y) '||' ((f . x),(f . y)) by A1, Th34;

        then

         A10: (x,y,(f . y)) are_collinear by A5, DIRAF:def 5;

        then (y,x,(f . y)) are_collinear by DIRAF: 30;

        then

         A11: (y,x) '||' (y,(f . y)) by DIRAF:def 5;

        

         A12: (y,(f . y),x) are_collinear by A10, DIRAF: 30;

         A13:

        now

          assume z = (f . z);

          then (z,y) '||' (z,(f . y)) by A1, Th34;

          then (z,y,(f . y)) are_collinear by DIRAF:def 5;

          then (y,(f . y),y) are_collinear & (y,(f . y),z) are_collinear by DIRAF: 30, DIRAF: 31;

          hence contradiction by A9, A12, A6, DIRAF: 32;

        end;

        (y,(f . y)) '||' (z,(f . z)) by A3;

        then (y,(f . y)) '||' (x,z) by A13, A8, DIRAF: 23;

        then (y,x) '||' (x,z) by A9, A11, DIRAF: 23;

        then (x,y) '||' (x,z) by DIRAF: 22;

        hence contradiction by A6, DIRAF:def 5;

      end;

      now

        assume

         A14: f = ( id the carrier of OAS) or for z holds (f . z) <> z;

        let x, y;

        

         A15: (x,y) '||' ((f . x),(f . y)) by A1, Th34;

         A16:

        now

          assume

           A17: for z holds (f . z) <> z;

          assume

           A18: not (x,(f . x)) '||' (y,(f . y));

          then

          consider z such that

           A19: (x,(f . x),z) are_collinear and

           A20: (y,(f . y),z) are_collinear by A15, Th48;

          set t = (f . z);

          (x,(f . x),t) are_collinear by A1, A19, Th47;

          then

           A21: (x,(f . x)) '||' (z,t) by A19, DIRAF: 34;

          (y,(f . y),t) are_collinear by A1, A20, Th47;

          then

           A22: (y,(f . y)) '||' (z,t) by A20, DIRAF: 34;

          z <> t by A17;

          hence contradiction by A18, A21, A22, DIRAF: 23;

        end;

        f = ( id the carrier of OAS) implies (x,(f . x)) '||' (y,(f . y)) by DIRAF: 20;

        hence (x,(f . x)) '||' (y,(f . y)) by A14, A16;

      end;

      hence thesis by A2;

    end;

    theorem :: TRANSGEO:50

    

     Th50: f is dilatation & (f . a) = a & (f . b) = b & not (a,b,x) are_collinear implies (f . x) = x

    proof

      assume that

       A1: f is dilatation and

       A2: (f . a) = a and

       A3: (f . b) = b and

       A4: not (a,b,x) are_collinear ;

      (a,x) '||' (a,(f . x)) by A1, A2, Th34;

      then (a,x,(f . x)) are_collinear by DIRAF:def 5;

      then

       A5: (x,(f . x),a) are_collinear by DIRAF: 30;

      (b,x) '||' (b,(f . x)) by A1, A3, Th34;

      then (b,x,(f . x)) are_collinear by DIRAF:def 5;

      then

       A6: (x,(f . x),x) are_collinear & (x,(f . x),b) are_collinear by DIRAF: 30, DIRAF: 31;

      assume (f . x) <> x;

      hence contradiction by A4, A5, A6, DIRAF: 32;

    end;

    theorem :: TRANSGEO:51

    

     Th51: f is dilatation & (f . a) = a & (f . b) = b & a <> b implies f = ( id the carrier of OAS)

    proof

      assume that

       A1: f is dilatation and

       A2: (f . a) = a and

       A3: (f . b) = b and

       A4: a <> b;

      now

        let x;

         A5:

        now

          assume

           A6: (a,b,x) are_collinear ;

          now

            consider z such that

             A7: not (a,b,z) are_collinear by A4, DIRAF: 37;

            assume

             A8: x <> a;

            

             A9: not (a,z,x) are_collinear

            proof

              assume (a,z,x) are_collinear ;

              then

               A10: (a,x,z) are_collinear by DIRAF: 30;

              (a,x,a) are_collinear & (a,x,b) are_collinear by A6, DIRAF: 30, DIRAF: 31;

              hence contradiction by A8, A7, A10, DIRAF: 32;

            end;

            (f . z) = z by A1, A2, A3, A7, Th50;

            hence (f . x) = x by A1, A2, A9, Th50;

          end;

          hence (f . x) = x by A2;

        end;

         not (a,b,x) are_collinear implies (f . x) = x by A1, A2, A3, Th50;

        hence (f . x) = (( id the carrier of OAS) . x) by A5;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: TRANSGEO:52

    f is dilatation & g is dilatation & (f . a) = (g . a) & (f . b) = (g . b) implies a = b or f = g

    proof

      assume that

       A1: f is dilatation and

       A2: g is dilatation and

       A3: (f . a) = (g . a) and

       A4: (f . b) = (g . b);

      

       A5: (((g " ) * f) . b) = ((g " ) . (g . b)) by A4, FUNCT_2: 15

      .= b by Th2;

      

       A6: (g " ) is dilatation by A2, Th43;

      assume

       A7: a <> b;

      (((g " ) * f) . a) = ((g " ) . (g . a)) by A3, FUNCT_2: 15

      .= a by Th2;

      then

       A8: ((g " ) * f) = ( id the carrier of OAS) by A1, A7, A5, A6, Th44, Th51;

      now

        let x;

        ((g " ) . (f . x)) = (((g " ) * f) . x) by FUNCT_2: 15;

        then ((g " ) . (f . x)) = x by A8;

        hence (g . x) = (f . x) by Th2;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    definition

      let OAS;

      let f be Permutation of the carrier of OAS;

      :: TRANSGEO:def9

      attr f is translation means f is dilatation & (f = ( id the carrier of OAS) or for a holds a <> (f . a));

    end

    theorem :: TRANSGEO:53

    

     Th53: f is dilatation implies (f is translation iff for x, y holds (x,(f . x)) '||' (y,(f . y))) by Th49;

    theorem :: TRANSGEO:54

    

     Th54: f is translation & g is translation & (f . a) = (g . a) & not (a,(f . a),x) are_collinear implies (f . x) = (g . x)

    proof

      assume that

       A1: f is translation and

       A2: g is translation and

       A3: (f . a) = (g . a) and

       A4: not (a,(f . a),x) are_collinear ;

      set b = (f . a), y = (f . x), z = (g . x);

      

       A5: (a,x) '||' (b,z) & (a,b) '||' (x,z) by A2, A3, Th34, Th53;

      f is dilatation by A1;

      then

       A6: (a,x) '||' (b,y) by Th34;

      (a,b) '||' (x,y) by A1, Th53;

      hence thesis by A4, A6, A5, PASCH: 5;

    end;

    theorem :: TRANSGEO:55

    

     Th55: f is translation & g is translation & (f . a) = (g . a) implies f = g

    proof

      assume that

       A1: f is translation and

       A2: g is translation and

       A3: (f . a) = (g . a);

      set b = (f . a);

      

       A4: f is dilatation by A1;

       A5:

      now

        assume

         A6: a <> b;

        for x holds (f . x) = (g . x)

        proof

          let x;

          now

            assume

             A7: (a,b,x) are_collinear ;

            now

              

               A8: f <> ( id the carrier of OAS) by A6;

              then

               A9: (f . x) <> x by A1;

              assume x <> a;

              consider p such that

               A10: not (a,b,p) are_collinear by A6, DIRAF: 37;

              

               A11: (f . p) <> p by A1, A8;

              

               A12: not (p,(f . p),x) are_collinear

              proof

                

                 A13: (a,b,(f . x)) are_collinear by A4, A7, Th47;

                (a,b,a) are_collinear by DIRAF: 31;

                then

                 A14: (x,(f . x),a) are_collinear by A6, A7, A13, DIRAF: 32;

                

                 A15: (p,(f . p),p) are_collinear by DIRAF: 31;

                (a,b,b) are_collinear by DIRAF: 31;

                then

                 A16: (x,(f . x),b) are_collinear by A6, A7, A13, DIRAF: 32;

                assume

                 A17: (p,(f . p),x) are_collinear ;

                then (p,(f . p),(f . x)) are_collinear by A4, Th47;

                then (x,(f . x),p) are_collinear by A11, A17, A15, DIRAF: 32;

                hence contradiction by A10, A9, A14, A16, DIRAF: 32;

              end;

              (f . p) = (g . p) by A1, A2, A3, A10, Th54;

              hence thesis by A1, A2, A12, Th54;

            end;

            hence thesis by A3;

          end;

          hence thesis by A1, A2, A3, Th54;

        end;

        hence thesis by FUNCT_2: 63;

      end;

      b = a implies thesis by A1, A2, A3;

      hence thesis by A5;

    end;

    theorem :: TRANSGEO:56

    

     Th56: f is translation implies (f " ) is translation

    proof

       A1:

      now

        assume

         A2: for x holds (f . x) <> x;

        given y such that

         A3: ((f " ) . y) = y;

        (f . y) = y by A3, Th2;

        hence contradiction by A2;

      end;

      assume

       A4: f is translation;

      then f is dilatation;

      then

       A5: (f " ) is dilatation by Th43;

      f = ( id the carrier of OAS) implies (f " ) = ( id the carrier of OAS) by FUNCT_1: 45;

      hence thesis by A4, A5, A1;

    end;

    theorem :: TRANSGEO:57

    f is translation & g is translation implies (f * g) is translation

    proof

      assume that

       A1: f is translation and

       A2: g is translation;

      f is dilatation & g is dilatation by A1, A2;

      then

       A3: (f * g) is dilatation by Th44;

      now

        assume

         A4: (f * g) <> ( id the carrier of OAS);

        for x holds ((f * g) . x) <> x

        proof

          given x such that

           A5: ((f * g) . x) = x;

          (f . (g . x)) = x by A5, FUNCT_2: 15;

          then

           A6: (g . x) = ((f " ) . x) by Th2;

          (f " ) is translation by A1, Th56;

          then (f * g) = (f * (f " )) by A2, A6, Th55;

          hence contradiction by A4, FUNCT_2: 61;

        end;

        hence thesis by A3;

      end;

      hence thesis by A3;

    end;

    

     Lm5: f is translation & not (a,(f . a),b) are_collinear implies (a,b) // ((f . a),(f . b)) & (a,(f . a)) // (b,(f . b))

    proof

      assume that

       A1: f is translation and

       A2: not (a,(f . a),b) are_collinear ;

      f is dilatation by A1;

      then

       A3: (a,b) '||' ((f . a),(f . b)) by Th34;

      (a,(f . a)) '||' (b,(f . b)) by A1, Th53;

      hence thesis by A2, A3, PASCH: 14;

    end;

    

     Lm6: f is translation & a <> (f . a) & (a,(f . a),b) are_collinear implies (a,(f . a)) // (b,(f . b))

    proof

      assume that

       A1: f is translation and

       A2: a <> (f . a) and

       A3: (a,(f . a),b) are_collinear ;

      consider p such that

       A4: not (a,(f . a),p) are_collinear by A2, DIRAF: 37;

      

       A5: f is dilatation by A1;

      

       A6: f <> ( id the carrier of OAS) by A2;

      then

       A7: p <> (f . p) by A1;

      

       A8: b <> (f . b) by A1, A6;

       not (p,(f . p),b) are_collinear

      proof

        

         A9: (p,(f . p),p) are_collinear by DIRAF: 31;

        assume

         A10: (p,(f . p),b) are_collinear ;

        then (p,(f . p),(f . b)) are_collinear by A5, Th47;

        then

         A11: (b,(f . b),p) are_collinear by A7, A10, A9, DIRAF: 32;

        (a,(f . a),(f . b)) are_collinear & (a,(f . a),a) are_collinear by A3, A5, Th47, DIRAF: 31;

        then

         A12: (b,(f . b),a) are_collinear by A2, A3, DIRAF: 32;

        then (b,(f . b),(f . a)) are_collinear by A5, Th47;

        hence contradiction by A4, A8, A12, A11, DIRAF: 32;

      end;

      then

       A13: (p,(f . p)) // (b,(f . b)) by A1, Lm5;

       not (p,(f . p),a) are_collinear

      proof

        assume

         A14: (p,(f . p),a) are_collinear ;

        then (p,(f . p),p) are_collinear & (p,(f . p),(f . a)) are_collinear by A5, Th47, DIRAF: 31;

        hence contradiction by A4, A7, A14, DIRAF: 32;

      end;

      then (p,(f . p)) // (a,(f . a)) by A1, Lm5;

      hence thesis by A7, A13, ANALOAF:def 5;

    end;

    

     Lm7: f is translation & Mid (a,(f . a),b) & a <> (f . a) implies (a,b) // ((f . a),(f . b))

    proof

      assume that

       A1: f is translation and

       A2: Mid (a,(f . a),b) and

       A3: a <> (f . a);

      

       A4: (a,(f . a)) // (b,(f . b)) by A1, A2, A3, Lm6, DIRAF: 28;

      now

         Mid (b,(f . a),a) by A2, DIRAF: 9;

        then (b,(f . a)) // ((f . a),a) by DIRAF:def 3;

        then (b,(f . a)) // (b,a) by ANALOAF:def 5;

        then

         A5: (a,b) // ((f . a),b) by DIRAF: 2;

        (a,(f . a)) // ((f . a),b) by A2, DIRAF:def 3;

        then ((f . a),b) // (b,(f . b)) by A3, A4, ANALOAF:def 5;

        then

         A6: ((f . a),b) // ((f . a),(f . b)) by ANALOAF:def 5;

        assume b <> (f . a);

        hence thesis by A5, A6, DIRAF: 3;

      end;

      hence thesis by A1, A2, A3, Lm6, DIRAF: 28;

    end;

    

     Lm8: f is translation & a <> (f . a) & b <> (f . a) & Mid (a,b,(f . a)) implies (a,b) // ((f . a),(f . b))

    proof

      assume that

       A1: f is translation and

       A2: a <> (f . a) and

       A3: b <> (f . a) and

       A4: Mid (a,b,(f . a));

      

       A5: (a,b) // (b,(f . a)) by A4, DIRAF:def 3;

      

       A6: f is dilatation by A1;

      

       A7: (a,b,(f . a)) are_collinear by A4, DIRAF: 28;

      then

       A8: (a,(f . a),b) are_collinear by DIRAF: 30;

      

       A9: f <> ( id the carrier of OAS) by A2;

      now

        assume

         A10: a <> b;

         A11:

        now

          ((f . a),a,b) are_collinear by A7, DIRAF: 30;

          then ((f . a),a) '||' ((f . a),b) by DIRAF:def 5;

          then

           A12: (a,(f . a)) '||' (b,(f . a)) by DIRAF: 22;

          consider q such that

           A13: not (a,(f . a),q) are_collinear by A2, DIRAF: 37;

          consider x such that

           A14: (q,b) // (b,x) and

           A15: (q,a) // ((f . a),x) by A5, A10, ANALOAF:def 5;

          

           A16: (a,q) // (x,(f . a)) by A15, DIRAF: 2;

          

           A17: Mid (q,b,x) by A14, DIRAF:def 3;

          then

           A18: (x,b,q) are_collinear by DIRAF: 9, DIRAF: 28;

          

           A19: x <> (f . a)

          proof

            assume x = (f . a);

            then Mid (q,b,(f . a)) by A14, DIRAF:def 3;

            then (q,b,(f . a)) are_collinear by DIRAF: 28;

            then

             A20: ((f . a),b,q) are_collinear by DIRAF: 30;

            

             A21: (a,b,a) are_collinear by DIRAF: 31;

            ((f . a),b,a) are_collinear & ((f . a),b,b) are_collinear by A7, DIRAF: 30, DIRAF: 31;

            then (a,b,q) are_collinear by A3, A20, DIRAF: 32;

            hence contradiction by A7, A10, A13, A21, DIRAF: 32;

          end;

          

           A22: not (x,(f . a),b) are_collinear

          proof

            assume (x,(f . a),b) are_collinear ;

            then ((f . a),x,b) are_collinear by DIRAF: 30;

            then

             A23: ((f . a),x) '||' ((f . a),b) by DIRAF:def 5;

            ((f . a),b,a) are_collinear by A7, DIRAF: 30;

            then

             A24: ((f . a),b) '||' ((f . a),a) by DIRAF:def 5;

            (q,a) '||' ((f . a),x) by A15, DIRAF:def 4;

            then ((f . a),b) '||' (q,a) by A19, A23, DIRAF: 23;

            then ((f . a),a) '||' (q,a) by A3, A24, DIRAF: 23;

            then (a,(f . a)) '||' (a,q) by DIRAF: 22;

            hence contradiction by A13, DIRAF:def 5;

          end;

          (a,(f . a)) // (q,(f . q)) by A1, A13, Lm5;

          then (a,(f . a)) '||' (q,(f . q)) by DIRAF:def 4;

          then (b,(f . a)) '||' (q,(f . q)) by A2, A12, DIRAF: 23;

          then

           A25: ((f . a),b) '||' (q,(f . q)) by DIRAF: 22;

          

           A26: (a,(f . a),(f . b)) are_collinear by A6, A8, Th47;

          (a,q) // ((f . a),(f . q)) & a <> q by A1, A13, Lm5, DIRAF: 31;

          then ((f . a),(f . q)) // (x,(f . a)) by A16, ANALOAF:def 5;

          then ((f . a),(f . q)) '||' ((f . a),x) by DIRAF:def 4;

          then ((f . a),(f . q),x) are_collinear by DIRAF:def 5;

          then

           A27: (x,(f . a),(f . q)) are_collinear by DIRAF: 30;

          

           A28: b <> (f . b) by A1, A9;

          (a,(f . a),(f . a)) are_collinear by DIRAF: 31;

          then

           A29: (b,(f . b),(f . a)) are_collinear by A2, A8, A26, DIRAF: 32;

          (a,(f . a),a) are_collinear by DIRAF: 31;

          then (b,(f . b),a) are_collinear by A2, A8, A26, DIRAF: 32;

          then

           A30: not (b,(f . b),q) are_collinear by A13, A29, A28, DIRAF: 32;

          

           A31: not (b,(f . b),(f . q)) are_collinear

          proof

            (b,(f . b)) '||' (q,(f . q)) by A1, Th53;

            then

             A32: (b,(f . b)) '||' ((f . q),q) by DIRAF: 22;

            assume (b,(f . b),(f . q)) are_collinear ;

            hence contradiction by A28, A30, A32, DIRAF: 33;

          end;

          then

           A33: (f . b) <> (f . q) by DIRAF: 31;

          (a,b) // (a,(f . a)) & (a,(f . a)) // (b,(f . b)) by A1, A8, A5, Lm6, ANALOAF:def 5;

          then

           A34: (a,b) // (b,(f . b)) by A2, DIRAF: 3;

          assume (a,b) // ((f . b),(f . a));

          then (b,(f . b)) // ((f . b),(f . a)) by A10, A34, ANALOAF:def 5;

          then Mid (b,(f . b),(f . a)) by DIRAF:def 3;

          then

           A35: Mid ((f . a),(f . b),b) by DIRAF: 9;

          

           A36: (x,b,b) are_collinear by DIRAF: 31;

           Mid (x,b,q) by A17, DIRAF: 9;

          then Mid (x,(f . a),(f . q)) by A22, A27, A25, PASCH: 8;

          then

          consider y such that

           A37: Mid (x,y,b) and

           A38: Mid (y,(f . b),(f . q)) by A35, A22, PASCH: 27;

          (x,y,b) are_collinear by A37, DIRAF: 28;

          then

           A39: (x,b,y) are_collinear by DIRAF: 30;

          

           A40: x <> b by A22, DIRAF: 31;

          then (b,q,y) are_collinear by A18, A39, A36, DIRAF: 32;

          then

           A41: (b,q) '||' (b,y) by DIRAF:def 5;

          

           A42: (y,(f . b),(f . q)) are_collinear by A38, DIRAF: 28;

          then ((f . b),(f . q),y) are_collinear by DIRAF: 30;

          then

           A43: ((f . b),(f . q)) '||' ((f . b),y) by DIRAF:def 5;

          (b,q) '||' ((f . b),(f . q)) by A6, Th34;

          then (b,q) '||' ((f . b),y) by A33, A43, DIRAF: 23;

          then ((f . b),y) '||' (b,y) by A33, A41, DIRAF: 23;

          then (y,b) '||' (y,(f . b)) by DIRAF: 22;

          then

           A44: (y,b,(f . b)) are_collinear by DIRAF:def 5;

          

           A45: (y,b,b) are_collinear by DIRAF: 31;

          (y,b,q) are_collinear by A40, A18, A39, A36, DIRAF: 32;

          hence contradiction by A42, A30, A31, A44, A45, DIRAF: 32;

        end;

        (a,b) '||' ((f . a),(f . b)) by A6, Th34;

        hence thesis by A11, DIRAF:def 4;

      end;

      hence thesis by DIRAF: 4;

    end;

    

     Lm9: f is translation & a <> (f . a) & (a,(f . a),b) are_collinear implies (a,b) // ((f . a),(f . b))

    proof

      assume that

       A1: f is translation and

       A2: a <> (f . a) and

       A3: (a,(f . a),b) are_collinear ;

      f <> ( id the carrier of OAS) by A2;

      then

       A4: b <> (f . b) by A1;

      

       A5: f is dilatation by A1;

      now

        assume

         A6: a <> b;

         A7:

        now

          assume

           A8: Mid ((f . a),a,b);

           A9:

          now

            assume Mid ((f . b),b,a);

            then Mid (a,b,(f . b)) by DIRAF: 9;

            then (a,b) // (b,(f . b)) by DIRAF:def 3;

            then

             A10: (a,b) // (a,(f . b)) by ANALOAF:def 5;

             Mid (b,a,(f . a)) by A8, DIRAF: 9;

            then (b,a) // (a,(f . a)) by DIRAF:def 3;

            then

             A11: (a,b) // ((f . a),a) by ANALOAF:def 5;

            then ((f . a),a) // (a,(f . b)) by A6, A10, ANALOAF:def 5;

            then ((f . a),a) // ((f . a),(f . b)) by ANALOAF:def 5;

            hence thesis by A10, A11, DIRAF: 3;

          end;

           A12:

          now

             A13:

            now

              assume

               A14: a = (f . b);

              (a,(f . a)) // (b,(f . b)) by A1, A2, A3, Lm6;

              hence thesis by A14, DIRAF: 2;

            end;

            assume Mid (b,a,(f . b));

            then (b,a) // ((f . b),(f . a)) or a = (f . b) by A1, A4, Lm8;

            hence thesis by A13, DIRAF: 2;

          end;

           A15:

          now

            assume Mid (b,(f . b),a);

            then (b,a) // ((f . b),(f . a)) by A1, A4, Lm7;

            hence thesis by DIRAF: 2;

          end;

          (a,(f . a),(f . b)) are_collinear & (a,(f . a),a) are_collinear by A3, A5, Th47, DIRAF: 31;

          hence thesis by A2, A3, A15, A12, A9, DIRAF: 29, DIRAF: 32;

        end;

         A16:

        now

          assume

           A17: Mid (a,b,(f . a));

          b = (f . a) implies thesis by A1, A2, A3, Lm6;

          hence thesis by A1, A2, A17, Lm8;

        end;

         Mid (a,(f . a),b) implies thesis by A1, A2, Lm7;

        hence thesis by A3, A7, A16, DIRAF: 29;

      end;

      hence thesis by DIRAF: 4;

    end;

    theorem :: TRANSGEO:58

    

     Th58: f is translation implies f is positive_dilatation

    proof

      assume

       A1: f is translation;

       A2:

      now

        assume

         A3: for x holds (f . x) <> x;

        for a, b holds (a,b) // ((f . a),(f . b))

        proof

          let a, b;

          

           A4: a <> (f . a) by A3;

           not (a,(f . a),b) are_collinear implies (a,b) // ((f . a),(f . b)) by A1, Lm5;

          hence thesis by A1, A4, Lm9;

        end;

        hence thesis by Th27;

      end;

      f = ( id the carrier of OAS) implies thesis by Th28;

      hence thesis by A1, A2;

    end;

    theorem :: TRANSGEO:59

    

     Th59: f is dilatation & (f . p) = p & Mid (q,p,(f . q)) & not (p,q,x) are_collinear implies Mid (x,p,(f . x))

    proof

      assume that

       A1: f is dilatation and

       A2: (f . p) = p and

       A3: Mid (q,p,(f . q)) & not (p,q,x) are_collinear ;

      (q,x) '||' ((f . q),(f . x)) by A1, Th34;

      then

       A4: (q,x) '||' ((f . x),(f . q)) by DIRAF: 22;

      (p,x) '||' (p,(f . x)) by A1, A2, Th34;

      then (p,x,(f . x)) are_collinear by DIRAF:def 5;

      hence thesis by A3, A4, PASCH: 6;

    end;

    theorem :: TRANSGEO:60

    

     Th60: f is dilatation & (f . p) = p & Mid (q,p,(f . q)) & q <> p implies Mid (x,p,(f . x))

    proof

      assume that

       A1: f is dilatation & (f . p) = p and

       A2: Mid (q,p,(f . q)) and

       A3: q <> p;

      now

        consider r such that

         A4: not (p,q,r) are_collinear by A3, DIRAF: 37;

        assume

         A5: (p,q,x) are_collinear ;

        

         A6: x = p or not (p,r,x) are_collinear

        proof

          

           A7: (p,x,q) are_collinear & (p,x,p) are_collinear by A5, DIRAF: 30, DIRAF: 31;

          assume that

           A8: x <> p and

           A9: (p,r,x) are_collinear ;

          (p,x,r) are_collinear by A9, DIRAF: 30;

          hence contradiction by A4, A8, A7, DIRAF: 32;

        end;

         Mid (r,p,(f . r)) by A1, A2, A4, Th59;

        hence thesis by A1, A6, Th59, DIRAF: 10;

      end;

      hence thesis by A1, A2, Th59;

    end;

    theorem :: TRANSGEO:61

    

     Th61: f is dilatation & (f . p) = p & q <> p & Mid (q,p,(f . q)) & not (p,x,y) are_collinear implies (x,y) // ((f . y),(f . x))

    proof

      assume

       A1: f is dilatation;

      assume

       A2: (f . p) = p & q <> p & Mid (q,p,(f . q));

      then Mid (x,p,(f . x)) by A1, Th60;

      then

       A3: (x,p) // (p,(f . x)) by DIRAF:def 3;

       Mid (y,p,(f . y)) by A1, A2, Th60;

      then

       A4: (y,p) // (p,(f . y)) by DIRAF:def 3;

      (x,y) '||' ((f . x),(f . y)) by A1, Th34;

      hence thesis by A3, A4, PASCH: 12;

    end;

    theorem :: TRANSGEO:62

    

     Th62: f is dilatation & (f . p) = p & q <> p & Mid (q,p,(f . q)) & (p,x,y) are_collinear implies (x,y) // ((f . y),(f . x))

    proof

      assume that

       A1: f is dilatation and

       A2: (f . p) = p and

       A3: q <> p & Mid (q,p,(f . q)) and

       A4: (p,x,y) are_collinear ;

      

       A5: Mid (y,p,(f . y)) by A1, A2, A3, Th60;

       A6:

      now

        assume

         A7: x = p;

        then (y,x) // (x,(f . y)) by A5, DIRAF:def 3;

        hence thesis by A2, A7, DIRAF: 2;

      end;

       A8:

      now

        assume that

         A9: x <> p and y <> p and

         A10: x <> y;

        consider u such that

         A11: not (p,x,u) are_collinear by A9, DIRAF: 37;

        consider r such that

         A12: (x,y) '||' (u,r) and

         A13: (x,u) '||' (y,r) by DIRAF: 26;

        

         A14: not (x,y,u) are_collinear

        proof

          assume

           A15: (x,y,u) are_collinear ;

          (x,y,p) are_collinear & (x,y,x) are_collinear by A4, DIRAF: 30, DIRAF: 31;

          hence contradiction by A10, A11, A15, DIRAF: 32;

        end;

        then

         A16: (x,y) // (u,r) by A12, A13, PASCH: 14;

        

         A17: not (p,u,r) are_collinear

        proof

           A18:

          now

            assume u = r;

            then (u,x) '||' (u,y) by A13, DIRAF: 22;

            then (u,x,y) are_collinear by DIRAF:def 5;

            hence contradiction by A14, DIRAF: 30;

          end;

          (x,y,p) are_collinear by A4, DIRAF: 30;

          then (x,y) '||' (x,p) by DIRAF:def 5;

          then (x,y) '||' (p,x) by DIRAF: 22;

          then

           A19: (u,r) '||' (p,x) by A10, A12, DIRAF: 23;

          

           A20: (u,r,u) are_collinear by DIRAF: 31;

          assume (p,u,r) are_collinear ;

          then

           A21: (u,r,p) are_collinear by DIRAF: 30;

          (p,x) '||' (p,y) by A4, DIRAF:def 5;

          then (u,r) '||' (p,y) by A9, A19, DIRAF: 23;

          then

           A22: (u,r,y) are_collinear by A18, A21, DIRAF: 33;

          (u,r,x) are_collinear by A18, A21, A19, DIRAF: 33;

          hence contradiction by A14, A18, A22, A20, DIRAF: 32;

        end;

        then

         A23: u <> r by DIRAF: 31;

        set u9 = (f . u), r9 = (f . r), x9 = (f . x), y9 = (f . y);

        

         A24: not (x9,y9,u9) are_collinear by A1, A14, Th46;

        (x9,y9) '||' (u9,r9) & (x9,u9) '||' (y9,r9) by A1, A12, A13, Th45;

        then (x9,y9) // (u9,r9) by A24, PASCH: 14;

        then

         A25: (r9,u9) // (y9,x9) by DIRAF: 2;

        (u,r) // ((f . r),(f . u)) by A1, A2, A3, A17, Th61;

        then (x,y) // (r9,u9) by A16, A23, DIRAF: 3;

        hence thesis by A25, A23, DIRAF: 3, FUNCT_2: 58;

      end;

       Mid (x,p,(f . x)) by A1, A2, A3, Th60;

      hence thesis by A2, A6, A8, DIRAF: 4, DIRAF:def 3;

    end;

    theorem :: TRANSGEO:63

    

     Th63: f is dilatation & (f . p) = p & q <> p & Mid (q,p,(f . q)) implies f is negative_dilatation

    proof

      assume

       A1: f is dilatation & (f . p) = p & q <> p & Mid (q,p,(f . q));

      (x,y) // ((f . y),(f . x))

      proof

         not (p,x,y) are_collinear implies (x,y) // ((f . y),(f . x)) by A1, Th61;

        hence thesis by A1, Th62;

      end;

      hence thesis;

    end;

    theorem :: TRANSGEO:64

    

     Th64: f is dilatation & (f . p) = p & (for x holds (p,x) // (p,(f . x))) implies for y, z holds (y,z) // ((f . y),(f . z))

    proof

      assume that

       A1: f is dilatation and

       A2: (f . p) = p and

       A3: (p,x) // (p,(f . x));

      

       A4: not (p,y,z) are_collinear implies (y,z) // ((f . y),(f . z))

      proof

        assume

         A5: not (p,y,z) are_collinear ;

        

         A6: (p,y) // (p,(f . y)) & (p,z) // (p,(f . z)) by A3;

        (y,z) '||' ((f . y),(f . z)) by A1, Th34;

        hence thesis by A5, A6, PASCH: 13;

      end;

      let y, z;

      (p,y,z) are_collinear implies (y,z) // ((f . y),(f . z))

      proof

        assume

         A7: (p,y,z) are_collinear ;

         A8:

        now

          assume that

           A9: p <> y and

           A10: y <> z and z <> p;

          consider q such that

           A11: not (p,y,q) are_collinear by A9, DIRAF: 37;

          

           A12: not (y,z,q) are_collinear

          proof

            assume

             A13: (y,z,q) are_collinear ;

            (y,z,p) are_collinear & (y,z,y) are_collinear by A7, DIRAF: 30, DIRAF: 31;

            hence contradiction by A10, A11, A13, DIRAF: 32;

          end;

          then

           A14: not ((f . y),(f . z),(f . q)) are_collinear by A1, Th46;

          consider r such that

           A15: (y,z) '||' (q,r) and

           A16: (y,q) '||' (z,r) by DIRAF: 26;

          ((f . y),(f . z)) '||' ((f . q),(f . r)) & ((f . y),(f . q)) '||' ((f . z),(f . r)) by A1, A15, A16, Th45;

          then ((f . y),(f . z)) // ((f . q),(f . r)) by A14, PASCH: 14;

          then

           A17: ((f . q),(f . r)) // ((f . y),(f . z)) by DIRAF: 2;

          

           A18: q <> r

          proof

            assume q = r;

            then (q,y) '||' (q,z) by A16, DIRAF: 22;

            then (q,y,z) are_collinear by DIRAF:def 5;

            hence contradiction by A12, DIRAF: 30;

          end;

           not (p,q,r) are_collinear

          proof

            

             A19: (q,r,q) are_collinear by DIRAF: 31;

            assume (p,q,r) are_collinear ;

            then

             A20: (q,r,p) are_collinear by DIRAF: 30;

            (y,p,z) are_collinear by A7, DIRAF: 30;

            then (y,p) '||' (y,z) by DIRAF:def 5;

            then (y,z) '||' (p,y) by DIRAF: 22;

            then (q,r) '||' (p,y) by A10, A15, DIRAF: 23;

            then (q,r,y) are_collinear by A18, A20, DIRAF: 33;

            hence contradiction by A11, A18, A20, A19, DIRAF: 32;

          end;

          then

           A21: (q,r) // ((f . q),(f . r)) by A4;

          (y,z) // (q,r) by A15, A16, A12, PASCH: 14;

          then (y,z) // ((f . q),(f . r)) by A18, A21, DIRAF: 3;

          hence thesis by A18, A17, DIRAF: 3, FUNCT_2: 58;

        end;

        now

          assume p = z;

          then (z,y) // ((f . z),(f . y)) by A2, A3;

          hence thesis by DIRAF: 2;

        end;

        hence thesis by A2, A3, A8, DIRAF: 4;

      end;

      hence thesis by A4;

    end;

    theorem :: TRANSGEO:65

    f is dilatation implies f is positive_dilatation or f is negative_dilatation

    proof

      assume

       A1: f is dilatation;

       A2:

      now

        given p such that

         A3: (f . p) = p;

         A4:

        now

          given q such that

           A5: not (p,q) // (p,(f . q));

          (p,q) '||' (p,(f . q)) by A1, A3, Th34;

          then

           A6: (p,q) // ((f . q),p) by A5, DIRAF:def 4;

          then (q,p) // (p,(f . q)) by DIRAF: 2;

          then

           A7: Mid (q,p,(f . q)) by DIRAF:def 3;

          p <> q by A5, A6, DIRAF: 2;

          hence f is negative_dilatation by A1, A3, A7, Th63;

        end;

        now

          assume for x holds (p,x) // (p,(f . x));

          then for x, y holds (x,y) // ((f . x),(f . y)) by A1, A3, Th64;

          hence f is positive_dilatation by Th27;

        end;

        hence thesis by A4;

      end;

      now

        assume for x holds (f . x) <> x;

        then f is translation by A1;

        hence f is positive_dilatation by Th58;

      end;

      hence thesis by A2;

    end;

    reserve AFS for AffinSpace;

    reserve a,b,c,d,d1,d2,p,x,y,z,t for Element of AFS;

    theorem :: TRANSGEO:66

    

     Th66: AFS is CongrSpace-like by AFF_1: 5, AFF_1: 3, AFF_1: 4, AFF_1: 2;

    theorem :: TRANSGEO:67

    ( Lambda OAS) is CongrSpace

    proof

      ( Lambda OAS) is AffinSpace by DIRAF: 41;

      hence thesis by Th66;

    end;

    reserve f,g for Permutation of the carrier of AFS;

    definition

      let AFS;

      let f;

      :: TRANSGEO:def10

      attr f is dilatation means f is_DIL_of AFS;

    end

    theorem :: TRANSGEO:68

    

     Th68: f is dilatation iff for a, b holds (a,b) // ((f . a),(f . b)) by Th22;

    theorem :: TRANSGEO:69

    

     Th69: ( id the carrier of AFS) is dilatation

    proof

      for x, y holds (x,y) // ((( id the carrier of AFS) . x),(( id the carrier of AFS) . y)) by AFF_1: 2;

      hence thesis by Th68;

    end;

    theorem :: TRANSGEO:70

    

     Th70: f is dilatation implies (f " ) is dilatation

    proof

      assume

       A1: f is dilatation;

      now

        let x, y;

        set x9 = ((f " ) . x);

        set y9 = ((f " ) . y);

        (f . x9) = x & (f . y9) = y by Th2;

        then (x9,y9) // (x,y) by A1, Th68;

        hence (x,y) // (((f " ) . x),((f " ) . y)) by AFF_1: 4;

      end;

      hence thesis by Th68;

    end;

    theorem :: TRANSGEO:71

    

     Th71: f is dilatation & g is dilatation implies (f * g) is dilatation

    proof

      assume

       A1: f is dilatation & g is dilatation;

      now

        let x, y;

        set x9 = (g . x);

        set y9 = (g . y);

        

         A2: ((f * g) . x) = (f . x9) & ((f * g) . y) = (f . y9) by FUNCT_2: 15;

         A3:

        now

          assume x9 = y9;

          then x = y by FUNCT_2: 58;

          hence (x,y) // (((f * g) . x),((f * g) . y)) by AFF_1: 3;

        end;

        (x,y) // (x9,y9) & (x9,y9) // ((f . x9),(f . y9)) by A1, Th68;

        hence (x,y) // (((f * g) . x),((f * g) . y)) by A2, A3, AFF_1: 5;

      end;

      hence thesis by Th68;

    end;

    theorem :: TRANSGEO:72

    

     Th72: f is dilatation implies for a, b, c, d holds (a,b) // (c,d) iff ((f . a),(f . b)) // ((f . c),(f . d))

    proof

      assume

       A1: f is dilatation;

      let a, b, c, d;

      

       A2: (c,d) // ((f . c),(f . d)) by A1, Th68;

      

       A3: (a,b) // ((f . a),(f . b)) by A1, Th68;

       A4:

      now

         A5:

        now

           A6:

          now

            assume (f . c) = (f . d);

            then c = d by FUNCT_2: 58;

            hence (a,b) // (c,d) by AFF_1: 3;

          end;

          assume (a,b) // ((f . c),(f . d));

          hence (a,b) // (c,d) by A2, A6, AFF_1: 5;

        end;

         A7:

        now

          assume (f . a) = (f . b);

          then a = b by FUNCT_2: 58;

          hence (a,b) // (c,d) by AFF_1: 3;

        end;

        assume ((f . a),(f . b)) // ((f . c),(f . d));

        hence (a,b) // (c,d) by A3, A7, A5, AFF_1: 5;

      end;

      now

         A8:

        now

          

           A9: c = d implies ((f . a),(f . b)) // ((f . c),(f . d)) by AFF_1: 3;

          assume ((f . a),(f . b)) // (c,d);

          hence ((f . a),(f . b)) // ((f . c),(f . d)) by A2, A9, AFF_1: 5;

        end;

        assume (a,b) // (c,d);

        then ((f . a),(f . b)) // (c,d) or a = b by A3, AFF_1: 5;

        hence ((f . a),(f . b)) // ((f . c),(f . d)) by A8, AFF_1: 3;

      end;

      hence thesis by A4;

    end;

    theorem :: TRANSGEO:73

    f is dilatation implies for a, b, c holds LIN (a,b,c) iff LIN ((f . a),(f . b),(f . c))

    proof

      assume

       A1: f is dilatation;

      let a, b, c;

      (a,b) // (a,c) iff ((f . a),(f . b)) // ((f . a),(f . c)) by A1, Th72;

      hence thesis by AFF_1:def 1;

    end;

    theorem :: TRANSGEO:74

    

     Th74: f is dilatation & LIN (x,(f . x),y) implies LIN (x,(f . x),(f . y))

    proof

      assume

       A1: f is dilatation;

      assume

       A2: LIN (x,(f . x),y);

      now

        assume

         A3: x <> y;

        (x,(f . x)) // (x,y) & (x,y) // ((f . x),(f . y)) by A1, A2, Th68, AFF_1:def 1;

        then (x,(f . x)) // ((f . x),(f . y)) by A3, AFF_1: 5;

        then ((f . x),x) // ((f . x),(f . y)) by AFF_1: 4;

        then LIN ((f . x),x,(f . y)) by AFF_1:def 1;

        hence thesis by AFF_1: 6;

      end;

      hence thesis by AFF_1: 7;

    end;

    theorem :: TRANSGEO:75

    

     Th75: (a,b) // (c,d) implies ((a,c) // (b,d) or ex x st LIN (a,c,x) & LIN (b,d,x))

    proof

      assume

       A1: (a,b) // (c,d);

      assume

       A2: not (a,c) // (b,d);

       A3:

      now

        consider z such that

         A4: (a,b) // (c,z) and

         A5: (a,c) // (b,z) by DIRAF: 40;

        assume

         A6: a <> b;

         A7:

        now

          (c,d) // (c,z) by A1, A6, A4, AFF_1: 5;

          then LIN (c,d,z) by AFF_1:def 1;

          then LIN (d,c,z) by AFF_1: 6;

          then (d,c) // (d,z) by AFF_1:def 1;

          then (z,d) // (d,c) by AFF_1: 4;

          then

          consider t such that

           A8: (b,d) // (d,t) and

           A9: (b,z) // (c,t) by A2, A5, DIRAF: 40;

          assume b <> z;

          then (a,c) // (c,t) by A5, A9, AFF_1: 5;

          then (c,a) // (c,t) by AFF_1: 4;

          then LIN (c,a,t) by AFF_1:def 1;

          then

           A10: LIN (a,c,t) by AFF_1: 6;

          (d,b) // (d,t) by A8, AFF_1: 4;

          then LIN (d,b,t) by AFF_1:def 1;

          then LIN (b,d,t) by AFF_1: 6;

          hence thesis by A10;

        end;

        now

          assume b = z;

          then (b,a) // (b,c) by A4, AFF_1: 4;

          then LIN (b,a,c) by AFF_1:def 1;

          then

           A11: LIN (a,c,b) by AFF_1: 6;

           LIN (b,d,b) by AFF_1: 7;

          hence thesis by A11;

        end;

        hence thesis by A7;

      end;

      now

        assume a = b;

        then LIN (a,c,a) & LIN (b,d,a) by AFF_1: 7;

        hence thesis;

      end;

      hence thesis by A3;

    end;

    theorem :: TRANSGEO:76

    

     Th76: f is dilatation implies ((f = ( id the carrier of AFS) or for x holds (f . x) <> x) iff for x, y holds (x,(f . x)) // (y,(f . y)))

    proof

      assume

       A1: f is dilatation;

       A2:

      now

        assume

         A3: for x, y holds (x,(f . x)) // (y,(f . y));

        assume f <> ( id the carrier of AFS);

        then

        consider y such that

         A4: (f . y) <> (( id the carrier of AFS) . y) by FUNCT_2: 63;

        given x such that

         A5: (f . x) = x;

        x <> y by A5, A4;

        then

        consider z such that

         A6: not LIN (x,y,z) by AFF_1: 13;

        (x,z) // ((f . x),(f . z)) by A1, Th68;

        then LIN (x,z,(f . z)) by A5, AFF_1:def 1;

        then

         A7: LIN (z,(f . z),x) by AFF_1: 6;

         LIN (z,(f . z),z) by AFF_1: 7;

        then

         A8: (z,(f . z)) // (x,z) by A7, AFF_1: 10;

        

         A9: (f . y) <> y by A4;

        (x,y) // ((f . x),(f . y)) by A1, Th68;

        then

         A10: LIN (x,y,(f . y)) by A5, AFF_1:def 1;

        then LIN (y,x,(f . y)) by AFF_1: 6;

        then

         A11: (y,x) // (y,(f . y)) by AFF_1:def 1;

        

         A12: LIN (y,(f . y),x) by A10, AFF_1: 6;

         A13:

        now

          assume z = (f . z);

          then (z,y) // (z,(f . y)) by A1, Th68;

          then LIN (z,y,(f . y)) by AFF_1:def 1;

          then LIN (y,(f . y),y) & LIN (y,(f . y),z) by AFF_1: 6, AFF_1: 7;

          hence contradiction by A9, A12, A6, AFF_1: 8;

        end;

        (y,(f . y)) // (z,(f . z)) by A3;

        then (y,(f . y)) // (x,z) by A13, A8, AFF_1: 5;

        then (y,x) // (x,z) by A9, A11, AFF_1: 5;

        then (x,y) // (x,z) by AFF_1: 4;

        hence contradiction by A6, AFF_1:def 1;

      end;

      now

        assume

         A14: f = ( id the carrier of AFS) or for z holds (f . z) <> z;

        let x, y;

        

         A15: (x,y) // ((f . x),(f . y)) by A1, Th68;

         A16:

        now

          assume

           A17: for z holds (f . z) <> z;

          assume

           A18: not (x,(f . x)) // (y,(f . y));

          then

          consider z such that

           A19: LIN (x,(f . x),z) and

           A20: LIN (y,(f . y),z) by A15, Th75;

          set t = (f . z);

           LIN (x,(f . x),t) by A1, A19, Th74;

          then

           A21: (x,(f . x)) // (z,t) by A19, AFF_1: 10;

           LIN (y,(f . y),t) by A1, A20, Th74;

          then

           A22: (y,(f . y)) // (z,t) by A20, AFF_1: 10;

          z <> t by A17;

          hence contradiction by A18, A21, A22, AFF_1: 5;

        end;

        f = ( id the carrier of AFS) implies (x,(f . x)) // (y,(f . y)) by AFF_1: 3;

        hence (x,(f . x)) // (y,(f . y)) by A14, A16;

      end;

      hence thesis by A2;

    end;

    theorem :: TRANSGEO:77

    

     Th77: f is dilatation & (f . a) = a & (f . b) = b & not LIN (a,b,x) implies (f . x) = x

    proof

      assume that

       A1: f is dilatation and

       A2: (f . a) = a and

       A3: (f . b) = b and

       A4: not LIN (a,b,x);

      (a,x) // (a,(f . x)) by A1, A2, Th68;

      then LIN (a,x,(f . x)) by AFF_1:def 1;

      then

       A5: LIN (x,(f . x),a) by AFF_1: 6;

      (b,x) // (b,(f . x)) by A1, A3, Th68;

      then LIN (b,x,(f . x)) by AFF_1:def 1;

      then

       A6: LIN (x,(f . x),x) & LIN (x,(f . x),b) by AFF_1: 6, AFF_1: 7;

      assume (f . x) <> x;

      hence contradiction by A4, A5, A6, AFF_1: 8;

    end;

    theorem :: TRANSGEO:78

    

     Th78: f is dilatation & (f . a) = a & (f . b) = b & a <> b implies f = ( id the carrier of AFS)

    proof

      assume that

       A1: f is dilatation and

       A2: (f . a) = a and

       A3: (f . b) = b and

       A4: a <> b;

      now

        let x;

         A5:

        now

          assume

           A6: LIN (a,b,x);

          now

            consider z such that

             A7: not LIN (a,b,z) by A4, AFF_1: 13;

            assume

             A8: x <> a;

            

             A9: not LIN (a,z,x)

            proof

              assume LIN (a,z,x);

              then

               A10: LIN (a,x,z) by AFF_1: 6;

               LIN (a,x,a) & LIN (a,x,b) by A6, AFF_1: 6, AFF_1: 7;

              hence contradiction by A8, A7, A10, AFF_1: 8;

            end;

            (f . z) = z by A1, A2, A3, A7, Th77;

            hence (f . x) = x by A1, A2, A9, Th77;

          end;

          hence (f . x) = x by A2;

        end;

         not LIN (a,b,x) implies (f . x) = x by A1, A2, A3, Th77;

        hence (f . x) = (( id the carrier of AFS) . x) by A5;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: TRANSGEO:79

    f is dilatation & g is dilatation & (f . a) = (g . a) & (f . b) = (g . b) implies a = b or f = g

    proof

      assume that

       A1: f is dilatation and

       A2: g is dilatation and

       A3: (f . a) = (g . a) and

       A4: (f . b) = (g . b);

      

       A5: (((g " ) * f) . b) = ((g " ) . (g . b)) by A4, FUNCT_2: 15

      .= b by Th2;

      

       A6: (g " ) is dilatation by A2, Th70;

      assume

       A7: a <> b;

      (((g " ) * f) . a) = ((g " ) . (g . a)) by A3, FUNCT_2: 15

      .= a by Th2;

      then

       A8: ((g " ) * f) = ( id the carrier of AFS) by A1, A7, A5, A6, Th71, Th78;

      now

        let x;

        ((g " ) . (f . x)) = (((g " ) * f) . x) by FUNCT_2: 15;

        then ((g " ) . (f . x)) = x by A8;

        hence (g . x) = (f . x) by Th2;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: TRANSGEO:80

    

     Th80: not LIN (a,b,c) & (a,b) // (c,d1) & (a,b) // (c,d2) & (a,c) // (b,d1) & (a,c) // (b,d2) implies d1 = d2

    proof

      assume that

       A1: not LIN (a,b,c) and

       A2: (a,b) // (c,d1) and

       A3: (a,b) // (c,d2) and

       A4: (a,c) // (b,d1) and

       A5: (a,c) // (b,d2);

      assume

       A6: d1 <> d2;

      a <> c by A1, AFF_1: 7;

      then (b,d1) // (b,d2) by A4, A5, AFF_1: 5;

      then LIN (b,d1,d2) by AFF_1:def 1;

      then

       A7: LIN (d1,d2,b) by AFF_1: 6;

       A8:

      now

        assume c = d1;

        then (c,a) // (c,b) by A4, AFF_1: 4;

        then LIN (c,a,b) by AFF_1:def 1;

        hence contradiction by A1, AFF_1: 6;

      end;

      

       A9: LIN (d1,d2,d1) by AFF_1: 7;

      a <> b by A1, AFF_1: 7;

      then (c,d1) // (c,d2) by A2, A3, AFF_1: 5;

      then

       A10: LIN (c,d1,d2) by AFF_1:def 1;

      then

       A11: LIN (d1,d2,c) by AFF_1: 6;

       LIN (d1,d2,c) by A10, AFF_1: 6;

      then (d1,d2) // (c,d1) by A9, AFF_1: 10;

      then (d1,d2) // (a,b) or c = d1 by A2, AFF_1: 5;

      then (d1,d2) // (b,a) by A8, AFF_1: 4;

      then LIN (d1,d2,a) by A6, A7, AFF_1: 9;

      hence contradiction by A1, A6, A11, A7, AFF_1: 8;

    end;

    definition

      let AFS;

      let f;

      :: TRANSGEO:def11

      attr f is translation means f is dilatation & (f = ( id the carrier of AFS) or for a holds a <> (f . a));

    end

    theorem :: TRANSGEO:81

    ( id the carrier of AFS) is translation by Th69;

    theorem :: TRANSGEO:82

    

     Th82: f is dilatation implies (f is translation iff for x, y holds (x,(f . x)) // (y,(f . y))) by Th76;

    theorem :: TRANSGEO:83

    

     Th83: f is translation & g is translation & (f . a) = (g . a) & not LIN (a,(f . a),x) implies (f . x) = (g . x)

    proof

      assume that

       A1: f is translation and

       A2: g is translation and

       A3: (f . a) = (g . a) and

       A4: not LIN (a,(f . a),x);

      set b = (f . a), y = (f . x), z = (g . x);

      

       A5: (a,x) // (b,z) & (a,b) // (x,z) by A2, A3, Th68, Th82;

      f is dilatation by A1;

      then

       A6: (a,x) // (b,y) by Th68;

      (a,b) // (x,y) by A1, Th82;

      hence thesis by A4, A6, A5, Th80;

    end;

    theorem :: TRANSGEO:84

    

     Th84: f is translation & g is translation & (f . a) = (g . a) implies f = g

    proof

      assume that

       A1: f is translation and

       A2: g is translation and

       A3: (f . a) = (g . a);

      set b = (f . a);

      

       A4: f is dilatation by A1;

       A5:

      now

        assume

         A6: a <> b;

        for x holds (f . x) = (g . x)

        proof

          let x;

          now

            assume

             A7: LIN (a,b,x);

            now

              

               A8: f <> ( id the carrier of AFS) by A6;

              then

               A9: (f . x) <> x by A1;

              assume x <> a;

              consider p such that

               A10: not LIN (a,b,p) by A6, AFF_1: 13;

              

               A11: (f . p) <> p by A1, A8;

              

               A12: not LIN (p,(f . p),x)

              proof

                

                 A13: LIN (a,b,(f . x)) by A4, A7, Th74;

                 LIN (a,b,a) by AFF_1: 7;

                then

                 A14: LIN (x,(f . x),a) by A6, A7, A13, AFF_1: 8;

                

                 A15: LIN (p,(f . p),p) by AFF_1: 7;

                 LIN (a,b,b) by AFF_1: 7;

                then

                 A16: LIN (x,(f . x),b) by A6, A7, A13, AFF_1: 8;

                assume

                 A17: LIN (p,(f . p),x);

                then LIN (p,(f . p),(f . x)) by A4, Th74;

                then LIN (x,(f . x),p) by A11, A17, A15, AFF_1: 8;

                hence contradiction by A10, A9, A14, A16, AFF_1: 8;

              end;

              (f . p) = (g . p) by A1, A2, A3, A10, Th83;

              hence thesis by A1, A2, A12, Th83;

            end;

            hence thesis by A3;

          end;

          hence thesis by A1, A2, A3, Th83;

        end;

        hence thesis by FUNCT_2: 63;

      end;

      b = a implies thesis by A1, A2, A3;

      hence thesis by A5;

    end;

    theorem :: TRANSGEO:85

    

     Th85: f is translation implies (f " ) is translation

    proof

       A1:

      now

        assume

         A2: for x holds (f . x) <> x;

        given y such that

         A3: ((f " ) . y) = y;

        (f . y) = y by A3, Th2;

        hence contradiction by A2;

      end;

      assume

       A4: f is translation;

      then f is dilatation;

      then

       A5: (f " ) is dilatation by Th70;

      f = ( id the carrier of AFS) implies (f " ) = ( id the carrier of AFS) by FUNCT_1: 45;

      hence thesis by A4, A5, A1;

    end;

    theorem :: TRANSGEO:86

    f is translation & g is translation implies (f * g) is translation

    proof

      assume that

       A1: f is translation and

       A2: g is translation;

      f is dilatation & g is dilatation by A1, A2;

      then

       A3: (f * g) is dilatation by Th71;

      now

        assume

         A4: (f * g) <> ( id the carrier of AFS);

        for x holds ((f * g) . x) <> x

        proof

          given x such that

           A5: ((f * g) . x) = x;

          (f . (g . x)) = x by A5, FUNCT_2: 15;

          then

           A6: (g . x) = ((f " ) . x) by Th2;

          (f " ) is translation by A1, Th85;

          then (f * g) = (f * (f " )) by A2, A6, Th84;

          hence contradiction by A4, FUNCT_2: 61;

        end;

        hence thesis by A3;

      end;

      hence thesis by A3;

    end;

    definition

      let AFS;

      let f;

      :: TRANSGEO:def12

      attr f is collineation means f is_automorphism_of the CONGR of AFS;

    end

    theorem :: TRANSGEO:87

    

     Th87: f is collineation iff for x, y, z, t holds ((x,y) // (z,t) iff ((f . x),(f . y)) // ((f . z),(f . t)))

    proof

      thus f is collineation implies for x, y, z, t holds (x,y) // (z,t) iff ((f . x),(f . y)) // ((f . z),(f . t))

      proof

        assume

         A1: f is_automorphism_of the CONGR of AFS;

        let x, y, z, t;

        thus (x,y) // (z,t) implies ((f . x),(f . y)) // ((f . z),(f . t))

        proof

          assume (x,y) // (z,t);

          then [ [x, y], [z, t]] in the CONGR of AFS by ANALOAF:def 2;

          then [ [(f . x), (f . y)], [(f . z), (f . t)]] in the CONGR of AFS by A1;

          hence thesis by ANALOAF:def 2;

        end;

        assume ((f . x),(f . y)) // ((f . z),(f . t));

        then [ [(f . x), (f . y)], [(f . z), (f . t)]] in the CONGR of AFS by ANALOAF:def 2;

        then [ [x, y], [z, t]] in the CONGR of AFS by A1;

        hence thesis by ANALOAF:def 2;

      end;

      assume

       A2: for x, y, z, t holds ((x,y) // (z,t) iff ((f . x),(f . y)) // ((f . z),(f . t)));

      let x, y, z, t;

      (x,y) // (z,t) iff ((f . x),(f . y)) // ((f . z),(f . t)) by A2;

      hence thesis by ANALOAF:def 2;

    end;

    theorem :: TRANSGEO:88

    

     Th88: f is collineation implies ( LIN (x,y,z) iff LIN ((f . x),(f . y),(f . z)))

    proof

      assume f is collineation;

      then (x,y) // (x,z) iff ((f . x),(f . y)) // ((f . x),(f . z)) by Th87;

      hence thesis by AFF_1:def 1;

    end;

    theorem :: TRANSGEO:89

    f is collineation & g is collineation implies (f " ) is collineation & (f * g) is collineation & ( id the carrier of AFS) is collineation

    proof

      assume f is_automorphism_of the CONGR of AFS & g is_automorphism_of the CONGR of AFS;

      hence (f " ) is_automorphism_of the CONGR of AFS & (f * g) is_automorphism_of the CONGR of AFS by Th17, Th18;

      thus ( id the carrier of AFS) is_automorphism_of the CONGR of AFS;

    end;

    reserve A,C,K for Subset of AFS;

    theorem :: TRANSGEO:90

    

     Th90: a in A implies (f . a) in (f .: A)

    proof

      

       A1: ( dom f) = the carrier of AFS by FUNCT_2: 52;

      assume a in A;

      hence thesis by A1, FUNCT_1:def 6;

    end;

    theorem :: TRANSGEO:91

    

     Th91: x in (f .: A) iff ex y st y in A & (f . y) = x

    proof

      thus x in (f .: A) implies ex y st y in A & (f . y) = x

      proof

        assume x in (f .: A);

        then ex y be object st y in ( dom f) & y in A & x = (f . y) by FUNCT_1:def 6;

        hence thesis;

      end;

      given y such that

       A1: y in A & (f . y) = x;

      ( dom f) = the carrier of AFS by FUNCT_2: 52;

      hence thesis by A1, FUNCT_1:def 6;

    end;

    theorem :: TRANSGEO:92

    

     Th92: (f .: A) = (f .: C) implies A = C

    proof

      assume

       A1: (f .: A) = (f .: C);

      now

        let b be object;

        assume

         A2: b in C;

        then

        reconsider b9 = b as Element of AFS;

        set y = (f . b9);

        y in (f .: C) by A2, Th90;

        then ex a st a in A & (f . a) = y by A1, Th91;

        hence b in A by FUNCT_2: 58;

      end;

      then

       A3: C c= A by TARSKI:def 3;

      now

        let a be object;

        assume

         A4: a in A;

        then

        reconsider a9 = a as Element of AFS;

        set x = (f . a9);

        x in (f .: A) by A4, Th90;

        then ex b st b in C & (f . b) = x by A1, Th91;

        hence a in C by FUNCT_2: 58;

      end;

      then A c= C by TARSKI:def 3;

      hence thesis by A3, XBOOLE_0:def 10;

    end;

    theorem :: TRANSGEO:93

    

     Th93: f is collineation implies (f .: ( Line (a,b))) = ( Line ((f . a),(f . b)))

    proof

      assume

       A1: f is collineation;

      now

        let x be object;

        assume

         A2: x in ( Line ((f . a),(f . b)));

        then

        reconsider x9 = x as Element of AFS;

        consider y such that

         A3: (f . y) = x9 by Th1;

         LIN ((f . a),(f . b),(f . y)) by A2, A3, AFF_1:def 2;

        then LIN (a,b,y) by A1, Th88;

        then y in ( Line (a,b)) by AFF_1:def 2;

        hence x in (f .: ( Line (a,b))) by A3, Th91;

      end;

      then

       A4: ( Line ((f . a),(f . b))) c= (f .: ( Line (a,b))) by TARSKI:def 3;

      now

        let x be object;

        assume

         A5: x in (f .: ( Line (a,b)));

        then

        reconsider x9 = x as Element of AFS;

        consider y such that

         A6: y in ( Line (a,b)) and

         A7: (f . y) = x9 by A5, Th91;

         LIN (a,b,y) by A6, AFF_1:def 2;

        then LIN ((f . a),(f . b),x9) by A1, A7, Th88;

        hence x in ( Line ((f . a),(f . b))) by AFF_1:def 2;

      end;

      then (f .: ( Line (a,b))) c= ( Line ((f . a),(f . b))) by TARSKI:def 3;

      hence thesis by A4, XBOOLE_0:def 10;

    end;

    theorem :: TRANSGEO:94

    f is collineation & K is being_line implies (f .: K) is being_line

    proof

      assume that

       A1: f is collineation and

       A2: K is being_line;

      consider a, b such that

       A3: a <> b and

       A4: K = ( Line (a,b)) by A2, AFF_1:def 3;

      set q = (f . b);

      set p = (f . a);

      

       A5: p <> q by A3, FUNCT_2: 58;

      (f .: K) = ( Line (p,q)) by A1, A4, Th93;

      hence thesis by A5, AFF_1:def 3;

    end;

    theorem :: TRANSGEO:95

    

     Th95: f is collineation & A // C implies (f .: A) // (f .: C)

    proof

      assume that

       A1: f is collineation and

       A2: A // C;

      consider a, b, c, d such that

       A3: a <> b & c <> d and

       A4: (a,b) // (c,d) and

       A5: A = ( Line (a,b)) & C = ( Line (c,d)) by A2, AFF_1: 37;

      

       A6: ((f . a),(f . b)) // ((f . c),(f . d)) by A1, A4, Th87;

      

       A7: (f . a) <> (f . b) & (f . c) <> (f . d) by A3, FUNCT_2: 58;

      (f .: A) = ( Line ((f . a),(f . b))) & (f .: C) = ( Line ((f . c),(f . d))) by A1, A5, Th93;

      hence thesis by A7, A6, AFF_1: 37;

    end;

    reserve AFP for AffinPlane,

A,C,D,K for Subset of AFP,

a,b,c,d,p,x,y for Element of AFP,

f for Permutation of the carrier of AFP;

    theorem :: TRANSGEO:96

    (for A st A is being_line holds (f .: A) is being_line) implies f is collineation

    proof

      assume

       A1: for A st A is being_line holds (f .: A) is being_line;

      

       A2: a <> b implies (f .: ( Line (a,b))) = ( Line ((f . a),(f . b)))

      proof

        set A = ( Line (a,b));

        set x = (f . a);

        set y = (f . b);

        set K = ( Line (x,y));

        set M = (f .: A);

        assume

         A3: a <> b;

        then x <> y by FUNCT_2: 58;

        then

         A4: K is being_line by AFF_1:def 3;

        A is being_line by A3, AFF_1:def 3;

        then

         A5: M is being_line by A1;

        a in A by AFF_1: 15;

        then

         A6: x in M by Th90;

        b in A by AFF_1: 15;

        then

         A7: y in M by Th90;

        x in K & y in K by AFF_1: 15;

        hence thesis by A3, A4, A5, A6, A7, AFF_1: 18, FUNCT_2: 58;

      end;

      

       A8: (f .: A) is being_line implies A is being_line

      proof

        set K = (f .: A);

        assume (f .: A) is being_line;

        then

        consider x, y such that

         A9: x <> y and

         A10: K = ( Line (x,y)) by AFF_1:def 3;

        y in K by A10, AFF_1: 15;

        then

        consider b such that b in A and

         A11: (f . b) = y by Th91;

        x in K by A10, AFF_1: 15;

        then

        consider a such that a in A and

         A12: (f . a) = x by Th91;

        set C = ( Line (a,b));

        C is being_line & (f .: C) = K by A2, A9, A10, A12, A11, AFF_1:def 3;

        hence thesis by Th92;

      end;

      

       A13: (f .: A) // (f .: C) implies A // C

      proof

        set K = (f .: A);

        set M = (f .: C);

        assume

         A14: (f .: A) // (f .: C);

        then M is being_line by AFF_1: 36;

        then

         A15: C is being_line by A8;

        K is being_line by A14, AFF_1: 36;

        then

         A16: A is being_line by A8;

        now

          assume

           A17: A <> C;

          assume not A // C;

          then

          consider p such that

           A18: p in A & p in C by A16, A15, AFF_1: 58;

          set x = (f . p);

          x in K & x in M by A18, Th90;

          hence contradiction by A14, A17, Th92, AFF_1: 45;

        end;

        hence thesis by A16, AFF_1: 41;

      end;

      

       A19: ((f . a),(f . b)) // ((f . c),(f . d)) implies (a,b) // (c,d)

      proof

        set x = (f . a);

        set y = (f . b);

        set z = (f . c);

        set t = (f . d);

        assume

         A20: ((f . a),(f . b)) // ((f . c),(f . d));

        now

          set C = ( Line (c,d));

          set A = ( Line (a,b));

          set K = (f .: A);

          set M = (f .: C);

          

           A21: c in C & d in C by AFF_1: 15;

          assume

           A22: a <> b & c <> d;

          then

           A23: x <> y & z <> t by FUNCT_2: 58;

          K = ( Line (x,y)) & M = ( Line (z,t)) by A2, A22;

          then

           A24: K // M by A20, A23, AFF_1: 37;

          a in A & b in A by AFF_1: 15;

          hence thesis by A13, A21, A24, AFF_1: 39;

        end;

        hence thesis by AFF_1: 3;

      end;

      

       A25: A // C implies (f .: A) // (f .: C)

      proof

        assume

         A26: A // C;

        then C is being_line by AFF_1: 36;

        then

         A27: (f .: C) is being_line by A1;

        A is being_line by A26, AFF_1: 36;

        then

         A28: (f .: A) is being_line by A1;

        then

         A29: (f .: A) // (f .: A) by AFF_1: 41;

        A <> C implies (f .: A) // (f .: C)

        proof

          assume

           A30: A <> C;

          assume not (f .: A) // (f .: C);

          then

          consider x such that

           A31: x in (f .: A) and

           A32: x in (f .: C) by A28, A27, AFF_1: 58;

          consider b such that

           A33: b in C and

           A34: x = (f . b) by A32, Th91;

          consider a such that

           A35: a in A and

           A36: x = (f . a) by A31, Th91;

          a = b by A36, A34, FUNCT_2: 58;

          hence contradiction by A26, A30, A35, A33, AFF_1: 45;

        end;

        hence thesis by A29;

      end;

      (a,b) // (c,d) implies ((f . a),(f . b)) // ((f . c),(f . d))

      proof

        assume

         A37: (a,b) // (c,d);

        now

          set C = ( Line (c,d));

          set A = ( Line (a,b));

          set K = (f .: A);

          set M = (f .: C);

          a in A by AFF_1: 15;

          then

           A38: (f . a) in K by Th90;

          b in A by AFF_1: 15;

          then

           A39: (f . b) in K by Th90;

          d in C by AFF_1: 15;

          then

           A40: (f . d) in M by Th90;

          c in C by AFF_1: 15;

          then

           A41: (f . c) in M by Th90;

          assume a <> b & c <> d;

          then A // C by A37, AFF_1: 37;

          hence thesis by A25, A38, A39, A41, A40, AFF_1: 39;

        end;

        hence thesis by AFF_1: 3;

      end;

      hence thesis by A19, Th87;

    end;

    theorem :: TRANSGEO:97

    f is collineation & K is being_line & (for x st x in K holds (f . x) = x) & not p in K & (f . p) = p implies f = ( id the carrier of AFP)

    proof

      assume that

       A1: f is collineation and

       A2: K is being_line and

       A3: for x st x in K holds (f . x) = x and

       A4: not p in K and

       A5: (f . p) = p;

      

       A6: for x holds (f . x) = x

      proof

        let x;

        now

          assume not x in K;

          consider a, b such that

           A7: a in K and

           A8: b in K and

           A9: a <> b by A2, AFF_1: 19;

          set A = ( Line (p,a));

          

           A10: p in A by AFF_1: 15;

          (f .: A) = ( Line ((f . p),(f . a))) by A1, Th93;

          then

           A11: (f .: A) = A by A3, A5, A7;

          A is being_line by A4, A7, AFF_1:def 3;

          then

          consider C such that

           A12: x in C and

           A13: A // C by AFF_1: 49;

          

           A14: C is being_line by A13, AFF_1: 36;

          (f .: A) // (f .: C) by A1, A13, Th95;

          then

           A15: (f .: C) // C by A13, A11, AFF_1: 44;

          

           A16: a in A by AFF_1: 15;

           not C // K

          proof

            assume C // K;

            then A // K by A13, AFF_1: 44;

            hence contradiction by A4, A7, A10, A16, AFF_1: 45;

          end;

          then

          consider c such that

           A17: c in C and

           A18: c in K by A2, A14, AFF_1: 58;

          (f . c) = c by A3, A18;

          then c in (f .: C) by A17, Th90;

          then

           A19: (f .: C) = C by A17, A15, AFF_1: 45;

          set M = ( Line (p,b));

          

           A20: b in M by AFF_1: 15;

          (f .: M) = ( Line ((f . p),(f . b))) by A1, Th93;

          then

           A21: (f .: M) = M by A3, A5, A8;

          M is being_line by A4, A8, AFF_1:def 3;

          then

          consider D such that

           A22: x in D and

           A23: M // D by AFF_1: 49;

          

           A24: D is being_line by A23, AFF_1: 36;

          (f .: M) // (f .: D) by A1, A23, Th95;

          then

           A25: (f .: D) // D by A23, A21, AFF_1: 44;

          

           A26: p in M by AFF_1: 15;

           not D // K

          proof

            assume D // K;

            then M // K by A23, AFF_1: 44;

            hence contradiction by A4, A8, A26, A20, AFF_1: 45;

          end;

          then

          consider d such that

           A27: d in D and

           A28: d in K by A2, A24, AFF_1: 58;

          (f . d) = d by A3, A28;

          then d in (f .: D) by A27, Th90;

          then

           A29: (f .: D) = D by A27, A25, AFF_1: 45;

          

           A30: A is being_line by A13, AFF_1: 36;

          x = (f . x)

          proof

            assume

             A31: x <> (f . x);

            (f . x) in C & (f . x) in D by A12, A22, A19, A29, Th90;

            then C = D by A12, A22, A14, A24, A31, AFF_1: 18;

            then A // M by A13, A23, AFF_1: 44;

            then A = M by A10, A26, AFF_1: 45;

            hence contradiction by A2, A4, A7, A8, A9, A30, A10, A16, A20, AFF_1: 18;

          end;

          hence thesis;

        end;

        hence thesis by A3;

      end;

      for x holds (f . x) = (( id the carrier of AFP) . x) by A6;

      hence thesis by FUNCT_2: 63;

    end;