anproj10.miz



    begin

    registration

      let a,b,c,d be object;

      reduce ( <*a, b, c, d*> . 1) to a;

      reducibility by FINSEQ_4: 76;

      reduce ( <*a, b, c, d*> . 2) to b;

      reducibility by FINSEQ_4: 76;

      reduce ( <*a, b, c, d*> . 3) to c;

      reducibility by FINSEQ_4: 76;

      reduce ( <*a, b, c, d*> . 4) to d;

      reducibility by FINSEQ_4: 76;

    end

    theorem :: ANPROJ10:1

    for a,b,c,d,a9,b9,c9,d9 be object st <*a, b, c, d*> = <*a9, b9, c9, d9*> holds a = a9 & b = b9 & c = c9 & d = d9

    proof

      let a,b,c,d,a9,b9,c9,d9 be object;

      assume

       A1: <*a, b, c, d*> = <*a9, b9, c9, d9*>;

      set x = <*a, b, c, d*>, y = <*a9, b9, c9, d9*>;

      (x . 1) = a & (x . 2) = b & (x . 3) = c & (x . 4) = d & (y . 1) = a9 & (y . 2) = b9 & (y . 3) = c9 & (y . 4) = d9;

      hence thesis by A1;

    end;

    definition

      let r be Real;

      :: ANPROJ10:def1

      attr r is unit means

      : Def01: r = 1;

    end

    registration

      cluster non unit for non zero Real;

      existence

      proof

        take 2;

        thus thesis;

      end;

    end

    definition

      let r be non unit non zero Real;

      :: ANPROJ10:def2

      func op1 (r) -> non unit non zero Real equals (1 / r);

      coherence

      proof

        (1 / r) <> 1

        proof

          assume (1 / r) = 1;

          then (r * (1 / r)) = r;

          hence contradiction by Def01, XCMPLX_1: 106;

        end;

        hence thesis by Def01;

      end;

      involutiveness ;

    end

    definition

      let r be non unit non zero Real;

      :: ANPROJ10:def3

      func op2 (r) -> non unit non zero Real equals (1 - r);

      coherence

      proof

        r <> 0 ;

        then (1 - r) <> 0 & (1 - r) <> 1 by Def01;

        hence thesis by Def01;

      end;

      involutiveness ;

    end

    reserve a,b,r for non unit non zero Real;

    theorem :: ANPROJ10:2

    

     Th01: ( op2 ( op1 r)) = ((r - 1) / r) & ( op1 ( op2 r)) = (1 / (1 - r)) & ( op1 ( op2 ( op1 r))) = (r / (r - 1)) & ( op2 ( op1 ( op2 r))) = (r / (r - 1))

    proof

      

       A1: (1 - (1 / r)) = ((r / r) - (1 / r)) by XCMPLX_1: 60

      .= ((r - 1) / r);

      (1 - r) <> 0 by Def01;

      

      then (1 - (1 / (1 - r))) = (((1 - r) / (1 - r)) - (1 / (1 - r))) by XCMPLX_1: 60

      .= ( - (r / (1 - r)))

      .= (r / ( - (1 - r))) by XCMPLX_1: 188;

      hence thesis by A1, XCMPLX_1: 57;

    end;

    theorem :: ANPROJ10:3

    ( op2 ( op1 ( op2 ( op1 r)))) = ( op1 ( op2 r)) & ( op1 ( op2 ( op1 ( op2 r)))) = ( op2 ( op1 r))

    proof

      ( op2 ( op1 ( op2 ( op1 r)))) = (1 - (r / (r - 1))) & ( op1 ( op2 ( op1 ( op2 r)))) = (1 / (r / (r - 1))) by Th01;

      hence thesis;

    end;

    theorem :: ANPROJ10:4

    (( op1 a) / ( op1 b)) = (b / a);

    reserve X for non empty set,

x for Tuple of 4, X;

    theorem :: ANPROJ10:5

    

     Th02: (4 -tuples_on X) = the set of all <*d1, d2, d3, d4*> where d1,d2,d3,d4 be Element of X

    proof

      hereby

        let x be object;

        assume x in (4 -tuples_on X);

        then

        consider s be Element of (X * ) such that

         A1: x = s and

         A2: ( len s) = 4;

        1 in ( Seg 4) & 2 in ( Seg 4) & 3 in ( Seg 4) & 4 in ( Seg 4);

        then 1 in ( dom s) & 2 in ( dom s) & 3 in ( dom s) & 4 in ( dom s) by A2, FINSEQ_1:def 3;

        then

        reconsider d19 = (s . 1), d29 = (s . 2), d39 = (s . 3), d49 = (s . 4) as Element of X by FINSEQ_2: 11;

        s = <*d19, d29, d39, d49*> by A2, FINSEQ_4: 76;

        hence x in the set of all <*d1, d2, d3, d4*> where d1,d2,d3,d4 be Element of X by A1;

      end;

      let x be object;

      assume x in the set of all <*d1, d2, d3, d4*> where d1,d2,d3,d4 be Element of X;

      then

      consider d1,d2,d3,d4 be Element of X such that

       A3: x = <*d1, d2, d3, d4*>;

      ( len <*d1, d2, d3, d4*>) = 4 & <*d1, d2, d3, d4*> is Element of (X * ) by FINSEQ_1:def 11, FINSEQ_4: 76;

      hence x in (4 -tuples_on X) by A3;

    end;

    theorem :: ANPROJ10:6

    

     Th03: for a,b,c,d be object st (a = (x . 1) or a = (x . 2) or a = (x . 3) or a = (x . 4)) & (b = (x . 1) or b = (x . 2) or b = (x . 3) or b = (x . 4)) & (c = (x . 1) or c = (x . 2) or c = (x . 3) or c = (x . 4)) & (d = (x . 1) or d = (x . 2) or d = (x . 3) or d = (x . 4)) holds <*a, b, c, d*> is Tuple of 4, X

    proof

      let a,b,c,d be object;

      assume

       A1: (a = (x . 1) or a = (x . 2) or a = (x . 3) or a = (x . 4)) & (b = (x . 1) or b = (x . 2) or b = (x . 3) or b = (x . 4)) & (c = (x . 1) or c = (x . 2) or c = (x . 3) or c = (x . 4)) & (d = (x . 1) or d = (x . 2) or d = (x . 3) or d = (x . 4));

      set y = <*a, b, c, d*>;

      ( dom x) = ( Seg 4) by FINSEQ_2: 124;

      then

       A2: 1 in ( dom x) & 2 in ( dom x) & 3 in ( dom x) & 4 in ( dom x);

      reconsider d19 = (y . 1), d29 = (y . 2), d39 = (y . 3), d49 = (y . 4) as Element of X by A1, A2, FINSEQ_2: 11;

      a is Element of X & b is Element of X & c is Element of X & d is Element of X by A1, A2, FINSEQ_2: 11;

      then y in the set of all <*d1, d2, d3, d4*> where d1,d2,d3,d4 be Element of X;

      then y in (4 -tuples_on X) by Th02;

      hence thesis by FINSEQ_2: 131;

    end;

    definition

      let X be non empty set;

      let x be Tuple of 4, X;

      :: ANPROJ10:def4

      func pi_1342 (x) -> Tuple of 4, X equals <*(x . 1), (x . 3), (x . 4), (x . 2)*>;

      coherence by Th03;

      :: ANPROJ10:def5

      func pi_1423 (x) -> Tuple of 4, X equals <*(x . 1), (x . 4), (x . 2), (x . 3)*>;

      coherence by Th03;

      :: ANPROJ10:def6

      func pi_2143 (x) -> Tuple of 4, X equals <*(x . 2), (x . 1), (x . 4), (x . 3)*>;

      coherence by Th03;

      :: ANPROJ10:def7

      func pi_2314 (x) -> Tuple of 4, X equals <*(x . 2), (x . 3), (x . 1), (x . 4)*>;

      coherence by Th03;

      :: ANPROJ10:def8

      func pi_2341 (x) -> Tuple of 4, X equals <*(x . 2), (x . 3), (x . 4), (x . 1)*>;

      coherence by Th03;

      :: ANPROJ10:def9

      func pi_2413 (x) -> Tuple of 4, X equals <*(x . 2), (x . 4), (x . 1), (x . 3)*>;

      coherence by Th03;

      :: ANPROJ10:def10

      func pi_2431 (x) -> Tuple of 4, X equals <*(x . 2), (x . 4), (x . 3), (x . 1)*>;

      coherence by Th03;

      :: ANPROJ10:def11

      func pi_3124 (x) -> Tuple of 4, X equals <*(x . 3), (x . 1), (x . 2), (x . 4)*>;

      coherence by Th03;

      :: ANPROJ10:def12

      func pi_3142 (x) -> Tuple of 4, X equals <*(x . 3), (x . 1), (x . 4), (x . 2)*>;

      coherence by Th03;

      :: ANPROJ10:def13

      func pi_3241 (x) -> Tuple of 4, X equals <*(x . 3), (x . 2), (x . 4), (x . 1)*>;

      coherence by Th03;

      :: ANPROJ10:def14

      func pi_3412 (x) -> Tuple of 4, X equals <*(x . 3), (x . 4), (x . 1), (x . 2)*>;

      coherence by Th03;

      :: ANPROJ10:def15

      func pi_3421 (x) -> Tuple of 4, X equals <*(x . 3), (x . 4), (x . 2), (x . 1)*>;

      coherence by Th03;

      :: ANPROJ10:def16

      func pi_4123 (x) -> Tuple of 4, X equals <*(x . 4), (x . 1), (x . 2), (x . 3)*>;

      coherence by Th03;

      :: ANPROJ10:def17

      func pi_4132 (x) -> Tuple of 4, X equals <*(x . 4), (x . 1), (x . 3), (x . 2)*>;

      coherence by Th03;

      :: ANPROJ10:def18

      func pi_4213 (x) -> Tuple of 4, X equals <*(x . 4), (x . 2), (x . 1), (x . 3)*>;

      coherence by Th03;

      :: ANPROJ10:def19

      func pi_4312 (x) -> Tuple of 4, X equals <*(x . 4), (x . 3), (x . 1), (x . 2)*>;

      coherence by Th03;

      :: ANPROJ10:def20

      func pi_4321 (x) -> Tuple of 4, X equals <*(x . 4), (x . 3), (x . 2), (x . 1)*>;

      coherence by Th03;

    end

    definition

      let X be non empty set;

      let x be Tuple of 4, X;

      :: ANPROJ10:def21

      func pi_id (x) -> Tuple of 4, X equals <*(x . 1), (x . 2), (x . 3), (x . 4)*>;

      coherence by Th03;

      :: ANPROJ10:def22

      func pi_12 (x) -> Tuple of 4, X equals <*(x . 2), (x . 1), (x . 3), (x . 4)*>;

      coherence by Th03;

      involutiveness

      proof

        let x,PI be Tuple of 4, X;

        assume x = <*(PI . 2), (PI . 1), (PI . 3), (PI . 4)*>;

        then (x . 1) = (PI . 2) & (x . 2) = (PI . 1) & (x . 3) = (PI . 3) & (x . 4) = (PI . 4) & ( len PI) = 4 by CARD_1:def 7;

        hence thesis by FINSEQ_4: 76;

      end;

      :: ANPROJ10:def23

      func pi_13 (x) -> Tuple of 4, X equals <*(x . 3), (x . 2), (x . 1), (x . 4)*>;

      coherence by Th03;

      involutiveness

      proof

        let x,PI be Tuple of 4, X;

        assume x = <*(PI . 3), (PI . 2), (PI . 1), (PI . 4)*>;

        then (x . 1) = (PI . 3) & (x . 2) = (PI . 2) & (x . 3) = (PI . 1) & (x . 4) = (PI . 4) & ( len PI) = 4 by CARD_1:def 7;

        hence thesis by FINSEQ_4: 76;

      end;

      :: ANPROJ10:def24

      func pi_14 (x) -> Tuple of 4, X equals <*(x . 4), (x . 2), (x . 3), (x . 1)*>;

      coherence by Th03;

      involutiveness

      proof

        let x,PI be Tuple of 4, X;

        assume x = <*(PI . 4), (PI . 2), (PI . 3), (PI . 1)*>;

        then (x . 1) = (PI . 4) & (x . 2) = (PI . 2) & (x . 3) = (PI . 3) & (x . 4) = (PI . 1) & ( len PI) = 4 by CARD_1:def 7;

        hence thesis by FINSEQ_4: 76;

      end;

      :: ANPROJ10:def25

      func pi_23 (x) -> Tuple of 4, X equals <*(x . 1), (x . 3), (x . 2), (x . 4)*>;

      coherence by Th03;

      involutiveness

      proof

        let x,PI be Tuple of 4, X;

        assume x = <*(PI . 1), (PI . 3), (PI . 2), (PI . 4)*>;

        then (x . 1) = (PI . 1) & (x . 2) = (PI . 3) & (x . 3) = (PI . 2) & (x . 4) = (PI . 4) & ( len PI) = 4 by CARD_1:def 7;

        hence thesis by FINSEQ_4: 76;

      end;

      :: ANPROJ10:def26

      func pi_24 (x) -> Tuple of 4, X equals <*(x . 1), (x . 4), (x . 3), (x . 2)*>;

      coherence by Th03;

      involutiveness

      proof

        let x,PI be Tuple of 4, X;

        assume x = <*(PI . 1), (PI . 4), (PI . 3), (PI . 2)*>;

        then (x . 1) = (PI . 1) & (x . 2) = (PI . 4) & (x . 3) = (PI . 3) & (x . 4) = (PI . 2) & ( len PI) = 4 by CARD_1:def 7;

        hence thesis by FINSEQ_4: 76;

      end;

      :: ANPROJ10:def27

      func pi_34 (x) -> Tuple of 4, X equals <*(x . 1), (x . 2), (x . 4), (x . 3)*>;

      coherence by Th03;

      involutiveness

      proof

        let x,PI be Tuple of 4, X;

        assume x = <*(PI . 1), (PI . 2), (PI . 4), (PI . 3)*>;

        then (x . 1) = (PI . 1) & (x . 2) = (PI . 2) & (x . 3) = (PI . 4) & (x . 4) = (PI . 3) & ( len PI) = 4 by CARD_1:def 7;

        hence thesis by FINSEQ_4: 76;

      end;

    end

    registration

      let X be non empty set;

      let x be Tuple of 4, X;

      reduce ( pi_id x) to x;

      reducibility

      proof

        ( dom x) = ( Seg 4) by FINSEQ_2: 124;

        then ( len x) = 4 by FINSEQ_1:def 3;

        hence thesis by FINSEQ_4: 76;

      end;

    end

    notation

      let X be non empty set;

      let x be Tuple of 4, X;

      synonym pi_1234 (x) for pi_id (x);

      synonym pi_2134 (x) for pi_12 (x);

      synonym pi_3214 (x) for pi_13 (x);

      synonym pi_4231 (x) for pi_14 (x);

      synonym pi_1324 (x) for pi_23 (x);

      synonym pi_1432 (x) for pi_24 (x);

      synonym pi_1243 (x) for pi_34 (x);

    end

    theorem :: ANPROJ10:7

    ( pi_12 ( pi_13 x)) = ( pi_13 ( pi_23 x)) & ( pi_12 ( pi_14 x)) = ( pi_14 ( pi_24 x)) & ( pi_12 ( pi_23 x)) = ( pi_13 ( pi_12 x)) & ( pi_12 ( pi_24 x)) = ( pi_14 ( pi_12 x)) & ( pi_12 ( pi_34 x)) = ( pi_34 ( pi_12 x)) & ( pi_13 ( pi_12 x)) = ( pi_23 ( pi_13 x)) & ( pi_13 ( pi_14 x)) = ( pi_34 ( pi_13 x)) & ( pi_13 ( pi_23 x)) = ( pi_12 ( pi_13 x)) & ( pi_13 ( pi_24 x)) = ( pi_13 ( pi_24 x)) & ( pi_13 ( pi_34 x)) = ( pi_14 ( pi_13 x)) & ( pi_23 ( pi_12 x)) = ( pi_13 ( pi_23 x)) & ( pi_23 ( pi_13 x)) = ( pi_12 ( pi_23 x)) & ( pi_23 ( pi_14 x)) = ( pi_14 ( pi_23 x)) & ( pi_23 ( pi_24 x)) = ( pi_34 ( pi_23 x)) & ( pi_23 ( pi_34 x)) = ( pi_24 ( pi_23 x)) & ( pi_24 ( pi_12 x)) = ( pi_14 ( pi_24 x)) & ( pi_24 ( pi_13 x)) = ( pi_13 ( pi_24 x)) & ( pi_24 ( pi_14 x)) = ( pi_12 ( pi_24 x)) & ( pi_24 ( pi_23 x)) = ( pi_34 ( pi_24 x)) & ( pi_24 ( pi_34 x)) = ( pi_23 ( pi_24 x)) & ( pi_34 ( pi_12 x)) = ( pi_12 ( pi_34 x)) & ( pi_34 ( pi_13 x)) = ( pi_14 ( pi_34 x)) & ( pi_34 ( pi_14 x)) = ( pi_13 ( pi_34 x)) & ( pi_34 ( pi_23 x)) = ( pi_24 ( pi_34 x)) & ( pi_34 ( pi_24 x)) = ( pi_23 ( pi_34 x));

    theorem :: ANPROJ10:8

    ( pi_1342 x) = ( pi_34 ( pi_23 x)) & ( pi_1423 x) = ( pi_34 ( pi_24 x)) & ( pi_2143 x) = ( pi_12 ( pi_34 x)) & ( pi_2314 x) = ( pi_23 ( pi_12 x)) & ( pi_2341 x) = ( pi_34 ( pi_23 ( pi_12 x))) & ( pi_2413 x) = ( pi_34 ( pi_24 ( pi_12 x))) & ( pi_2431 x) = ( pi_24 ( pi_12 x)) & ( pi_3124 x) = ( pi_23 ( pi_13 x)) & ( pi_3142 x) = ( pi_24 ( pi_34 ( pi_13 x))) & ( pi_3241 x) = ( pi_34 ( pi_13 x)) & ( pi_3412 x) = ( pi_24 ( pi_13 x)) & ( pi_3421 x) = ( pi_24 ( pi_23 ( pi_13 x))) & ( pi_4123 x) = ( pi_23 ( pi_34 ( pi_14 x))) & ( pi_4132 x) = ( pi_24 ( pi_14 x)) & ( pi_4213 x) = ( pi_34 ( pi_14 x)) & ( pi_4312 x) = ( pi_23 ( pi_24 ( pi_14 x))) & ( pi_4321 x) = ( pi_23 ( pi_14 x));

    theorem :: ANPROJ10:9

    ( pi_13 ( pi_23 ( pi_13 x))) = ( pi_12 x) & ( pi_12 ( pi_34 ( pi_23 ( pi_13 x)))) = ( pi_34 ( pi_23 x)) & ( pi_23 ( pi_24 ( pi_14 ( pi_23 ( pi_13 x))))) = ( pi_14 x);

    theorem :: ANPROJ10:10

    ( pi_23 ( pi_14 ( pi_34 x))) = ( pi_24 ( pi_23 ( pi_13 x))) & ( pi_34 ( pi_24 ( pi_12 x))) = ( pi_24 ( pi_13 ( pi_23 x))) & ( pi_24 ( pi_34 ( pi_13 x))) = ( pi_12 ( pi_34 ( pi_23 x)));

    begin

    reserve V for RealLinearSpace,

A,B,C,P,Q,R,S for Element of V;

    theorem :: ANPROJ10:11

    

     Th05: (P,Q,Q) are_collinear

    proof

      P in ( Line (P,Q)) & Q in ( Line (P,Q)) by RLTOPSP1: 72;

      hence thesis;

    end;

    

     Lm01: for a,b be Real st A = (((1 - a) * P) + (a * Q)) & B = (((1 - b) * P) + (b * Q)) holds (A - B) = ((b - a) * (P - Q))

    proof

      let a,b be Real;

      assume that

       A1: A = (((1 - a) * P) + (a * Q)) and

       A2: B = (((1 - b) * P) + (b * Q));

      (A - B) = (((1 - a) * P) + ((a * Q) - (((1 - b) * P) + (b * Q)))) by A1, A2, RLVECT_1:def 3

      .= (((1 - a) * P) + (((a * Q) - (b * Q)) - ((1 - b) * P))) by RLVECT_1: 27

      .= (((1 - a) * P) + (((a - b) * Q) - ((1 - b) * P))) by RLVECT_1: 35

      .= ((((1 - a) * P) + ((a - b) * Q)) + ( - ((1 - b) * P))) by RLVECT_1:def 3

      .= ((((1 - a) * P) + ((a - b) * Q)) + (( - 1) * ((1 - b) * P))) by RLVECT_1: 16

      .= ((((1 - a) * P) + ((a - b) * Q)) + ((( - 1) * (1 - b)) * P)) by RLVECT_1:def 7

      .= (((1 - a) * P) + (((a - b) * Q) + ((b - 1) * P))) by RLVECT_1:def 3

      .= (((1 - a) * P) + (((b - 1) * P) + ((a - b) * Q))) by RLVECT_1:def 2

      .= ((((1 - a) * P) + ((b - 1) * P)) + ((a - b) * Q)) by RLVECT_1:def 3

      .= ((((1 - a) + (b - 1)) * P) + ((a - b) * Q)) by RLVECT_1:def 6

      .= (((b - a) * P) + ((( - 1) * (b - a)) * Q))

      .= (((b - a) * P) + (( - 1) * ((b - a) * Q))) by RLVECT_1:def 7

      .= (((b - a) * P) - ((( - 1) * (a - b)) * Q)) by RLVECT_1: 16;

      hence thesis by RLVECT_1: 34;

    end;

    definition

      let V be RealLinearSpace;

      let A,B,C be Element of V;

      assume that

       A1: A <> C and

       A2: (A,B,C) are_collinear ;

      :: ANPROJ10:def28

      func affine-ratio (A,B,C) -> Real means

      : Def02: (B - A) = (it * (C - A));

      existence

      proof

        consider L be line of V such that

         A3: A in L and

         A4: B in L and

         A5: C in L by A2;

        consider P,Q be Element of V such that

         A6: L = ( Line (P,Q)) by RLTOPSP1:def 15;

        

         A7: ( Line (P,Q)) = the set of all (((1 - r) * P) + (r * Q)) where r be Real by RLTOPSP1:def 14;

        consider a be Real such that

         A8: A = (((1 - a) * P) + (a * Q)) by A3, A6, A7;

        consider b be Real such that

         A9: B = (((1 - b) * P) + (b * Q)) by A4, A6, A7;

        consider c be Real such that

         A10: C = (((1 - c) * P) + (c * Q)) by A5, A6, A7;

        

         A11: (a - c) <> 0 by A8, A10, A1;

        set k = ((a - b) / (a - c));

        (B - A) = ((a - b) * (P - Q)) by A8, A9, Lm01

        .= ((((a - b) / (a - c)) * (a - c)) * (P - Q)) by A11, XCMPLX_1: 87

        .= (((a - b) / (a - c)) * ((a - c) * (P - Q))) by RLVECT_1:def 7

        .= (k * (C - A)) by A8, A10, Lm01;

        hence thesis;

      end;

      uniqueness

      proof

        let r1,r2 be Real such that

         A12: (B - A) = (r1 * (C - A)) and

         A13: (B - A) = (r2 * (C - A));

        (C - A) <> ( 0. V) & (r1 * (C - A)) = (r2 * (C - A)) by A12, A13, A1, RLVECT_1: 21;

        hence thesis by RLVECT_1: 37;

      end;

    end

    theorem :: ANPROJ10:12

    A <> C & (A,B,C) are_collinear implies (A - B) = (( affine-ratio (A,B,C)) * (A - C))

    proof

      assume that

       A1: A <> C and

       A2: (A,B,C) are_collinear ;

      (A - B) = ( - (B - A)) by RLVECT_1: 33

      .= ( - (( affine-ratio (A,B,C)) * (C - A))) by Def02, A1, A2

      .= (( - 1) * (( affine-ratio (A,B,C)) * (C - A))) by RLVECT_1: 16

      .= ((( - 1) * ( affine-ratio (A,B,C))) * (C - A)) by RLVECT_1:def 7

      .= (( affine-ratio (A,B,C)) * (( - 1) * (C - A))) by RLVECT_1:def 7

      .= (( affine-ratio (A,B,C)) * ( - (C - A))) by RLVECT_1: 16

      .= (( affine-ratio (A,B,C)) * (A - C)) by RLVECT_1: 33;

      hence thesis;

    end;

    theorem :: ANPROJ10:13

    

     Th06: A <> C & (A,B,C) are_collinear implies (( affine-ratio (A,B,C)) = 0 iff A = B)

    proof

      assume that

       A1: A <> C and

       A2: (A,B,C) are_collinear ;

      hereby

        assume ( affine-ratio (A,B,C)) = 0 ;

        

        then (B - A) = ( 0 * (C - A)) by A1, A2, Def02

        .= ( 0. V) by RLVECT_1: 10;

        hence A = B by RLVECT_1: 21;

      end;

      assume A = B;

      

      then (B - A) = ( 0. V) by RLVECT_1: 5

      .= ( 0 * (C - A)) by RLVECT_1: 10;

      hence ( affine-ratio (A,B,C)) = 0 by A1, A2, Def02;

    end;

    theorem :: ANPROJ10:14

    

     Th07: A <> C & (A,B,C) are_collinear implies (( affine-ratio (A,B,C)) = 1 iff B = C)

    proof

      assume that

       A1: A <> C and

       A2: (A,B,C) are_collinear ;

      hereby

        assume ( affine-ratio (A,B,C)) = 1;

        

        then (B - A) = (1 * (C - A)) by A1, A2, Def02

        .= (C - A) by RLVECT_1:def 8;

        hence B = C by RLVECT_1: 8;

      end;

      assume B = C;

      then (B - A) = (1 * (C - A)) by RLVECT_1:def 8;

      hence ( affine-ratio (A,B,C)) = 1 by A1, A2, Def02;

    end;

    theorem :: ANPROJ10:15

    

     Th08: for a,b be Real st P <> Q & (a * (P - Q)) = (b * (P - Q)) holds a = b

    proof

      let a,b be Real;

      assume that

       A1: P <> Q and

       A2: (a * (P - Q)) = (b * (P - Q));

      (P - Q) <> ( 0. V) by A1, RLVECT_1: 21;

      hence thesis by A2, RLVECT_1: 37;

    end;

    theorem :: ANPROJ10:16

    

     Th09: (P,Q,R) are_collinear & P <> R & P <> Q implies ( affine-ratio (P,R,Q)) = (1 / ( affine-ratio (P,Q,R)))

    proof

      assume that

       A1: (P,Q,R) are_collinear and

       A2: P <> R and

       A3: P <> Q;

      set r = ( affine-ratio (P,Q,R)), s = ( affine-ratio (P,R,Q));

      (P,R,Q) are_collinear by A1;

      

      then (R - P) = (s * (Q - P)) by A3, Def02

      .= (s * (r * (R - P))) by A1, A2, Def02

      .= ((s * r) * (R - P)) by RLVECT_1:def 7;

      then (1 * (R - P)) = ((s * r) * (R - P)) by RLVECT_1:def 8;

      hence thesis by A2, Th08, XCMPLX_1: 73;

    end;

    theorem :: ANPROJ10:17

    

     Th10: (P,Q,R) are_collinear & P <> R & Q <> R & P <> Q implies ( affine-ratio (Q,P,R)) = (( affine-ratio (P,Q,R)) / (( affine-ratio (P,Q,R)) - 1))

    proof

      assume that

       A1: (P,Q,R) are_collinear and

       A2: P <> R and

       A3: Q <> R and

       A4: P <> Q;

      set r = ( affine-ratio (P,Q,R)), s = ( affine-ratio (Q,P,R));

      

       A5: (Q - P) = (r * (R - P)) by A1, A2, Def02;

      (Q,P,R) are_collinear by A1;

      then (P - Q) = (s * (R - Q)) by A3, Def02;

      

      then (r * (R - P)) = ( - (s * ((R + ( 0. V)) - Q))) by A5, RLVECT_1: 33

      .= ( - (s * ((R + (( - P) + P)) - Q))) by RLVECT_1: 5

      .= ( - (s * (((R - P) + P) - Q))) by RLVECT_1:def 3

      .= ( - (s * ((R - P) + (P - Q)))) by RLVECT_1:def 3

      .= (( - 1) * (s * ((R - P) + (P - Q)))) by RLVECT_1: 16

      .= ((( - 1) * s) * ((R - P) + (P - Q))) by RLVECT_1:def 7

      .= ((( - s) * (R - P)) + (( - s) * (P - Q))) by RLVECT_1:def 5;

      

      then

       A6: ((r * (R - P)) + (s * (R - P))) = ((( - s) * (R - P)) + ((( - s) * (P - Q)) + (s * (R - P)))) by RLVECT_1:def 3

      .= ((( - s) * (R - P)) + ((s * (R - P)) + (( - s) * (P - Q)))) by RLVECT_1:def 2

      .= (((( - s) * (R - P)) + (s * (R - P))) + (( - s) * (P - Q))) by RLVECT_1:def 3

      .= (((( - s) + s) * (R - P)) + (( - s) * (P - Q))) by RLVECT_1:def 6

      .= (( 0. V) + (( - s) * (P - Q))) by RLVECT_1: 10

      .= (( - s) * (P - Q));

      (Q,P,R) are_collinear by A1;

      then

       A7: s <> 0 by A3, A4, Th06;

      then

      reconsider s9 = (1 / s) as non zero Real;

      

       A8: (s9 * s) = 1 by A7, XCMPLX_1: 106;

      

       A9: (r - 1) <> 0 by A1, A2, A3, Th07;

      ((r + s) * (R - P)) = (( - s) * (P - Q)) by A6, RLVECT_1:def 6

      .= (s * ( - (P - Q))) by RLVECT_1: 24

      .= (s * (Q - P)) by RLVECT_1: 33;

      

      then ((s9 * (r + s)) * (R - P)) = (s9 * (s * (Q - P))) by RLVECT_1:def 7

      .= ((s9 * s) * (Q - P)) by RLVECT_1:def 7

      .= (1 * (Q - P)) by A7, XCMPLX_1: 106

      .= (Q - P) by RLVECT_1:def 8;

      then (s * r) = (s * ((1 / s) * (r + s))) by A1, Def02, A2;

      then (r * s) = ((s * (1 / s)) * (r + s));

      then (r * s) = (r + s) by A8;

      then ((s * (r - 1)) / (r - 1)) = (r / (r - 1));

      then (s * ((r - 1) / (r - 1))) = (r / (r - 1));

      then (s * 1) = (r / (r - 1)) by A9, XCMPLX_1: 60;

      hence thesis;

    end;

    theorem :: ANPROJ10:18

    

     Th11: (P,Q,R) are_collinear & P <> R implies ( affine-ratio (R,Q,P)) = (1 - ( affine-ratio (P,Q,R)))

    proof

      assume that

       A1: (P,Q,R) are_collinear and

       A2: P <> R;

      set r = ( affine-ratio (P,Q,R)), s = ( affine-ratio (R,Q,P));

      

       A3: (Q - P) = (r * (R - P)) by A1, A2, Def02;

      

       A4: (Q - P) = ((Q + ( 0. V)) - P)

      .= ((Q + (( - R) + R)) - P) by RLVECT_1: 5

      .= (((Q + ( - R)) + R) - P) by RLVECT_1:def 3

      .= ((Q - R) + (R - P)) by RLVECT_1:def 3

      .= ((Q - R) - (P - R)) by RLVECT_1: 33;

      (R,Q,P) are_collinear by A1;

      

      then ((r * (R - P)) - (s * (P - R))) = (((s * (P - R)) - (P - R)) - (s * (P - R))) by A3, A4, A2, Def02

      .= (((s * (P - R)) + (R - P)) - (s * (P - R))) by RLVECT_1: 33

      .= ((s * (P - R)) + ((R - P) - (s * (P - R)))) by RLVECT_1:def 3

      .= ((s * (P - R)) + (( - (s * (P - R))) + (R - P))) by RLVECT_1:def 2

      .= (((s * (P - R)) - (s * (P - R))) + (R - P)) by RLVECT_1:def 3

      .= (( 0. V) + (R - P)) by RLVECT_1: 5

      .= (R - P);

      

      then (R - P) = ((r * (R - P)) - (s * ( - (R - P)))) by RLVECT_1: 33

      .= ((r * (R - P)) - (s * (( - 1) * (R - P)))) by RLVECT_1: 16

      .= ((r * (R - P)) - ((s * ( - 1)) * (R - P))) by RLVECT_1:def 7

      .= ((r * (R - P)) - (( - s) * (R - P)));

      

      then ((R - P) + (( - s) * (R - P))) = ((r * (R - P)) + (( - (( - s) * (R - P))) + (( - s) * (R - P)))) by RLVECT_1:def 3

      .= ((r * (R - P)) + ( 0. V)) by RLVECT_1: 5

      .= (r * (R - P));

      then ((1 * (R - P)) + (( - s) * (R - P))) = (r * (R - P)) by RLVECT_1:def 8;

      then ((1 - s) * (R - P)) = (r * (R - P)) by RLVECT_1:def 6;

      then (1 - s) = r by A2, Th08;

      hence thesis;

    end;

    theorem :: ANPROJ10:19

    

     Th12: (P,Q,R) are_collinear & P <> R & P <> Q implies ( affine-ratio (Q,R,P)) = ((( affine-ratio (P,Q,R)) - 1) / ( affine-ratio (P,Q,R)))

    proof

      assume that

       A1: (P,Q,R) are_collinear and

       A2: P <> R and

       A3: P <> Q;

      set r = ( affine-ratio (P,Q,R)), s = ( affine-ratio (Q,R,P));

      

       A4: r <> 0 by A1, A2, A3, Th06;

      

       A5: (Q - P) = (r * ((R + ( 0. V)) - P)) by A1, A2, Def02

      .= (r * ((R + (( - Q) + Q)) - P)) by RLVECT_1: 5

      .= (r * (((R + ( - Q)) + Q) - P)) by RLVECT_1:def 3

      .= (r * ((R - Q) + (Q - P))) by RLVECT_1:def 3

      .= ((r * (R - Q)) + (r * (Q - P))) by RLVECT_1:def 5;

      (Q,R,P) are_collinear by A1;

      

      then (Q - P) = ((r * (s * (P - Q))) + (r * (Q - P))) by A5, A3, Def02

      .= (((r * s) * (P - Q)) + (r * (Q - P))) by RLVECT_1:def 7

      .= (((r * s) * ( - (Q - P))) + (r * (Q - P))) by RLVECT_1: 33

      .= (((r * s) * (( - 1) * (Q - P))) + (r * (Q - P))) by RLVECT_1: 16

      .= ((((r * s) * ( - 1)) * (Q - P)) + (r * (Q - P))) by RLVECT_1:def 7

      .= ((( - (r * s)) + r) * (Q - P)) by RLVECT_1:def 6;

      then (1 * (Q - P)) = ((r - (r * s)) * (Q - P)) by RLVECT_1:def 8;

      then 1 = (r - (r * s)) by A3, Th08;

      hence thesis by A4, XCMPLX_1: 89;

    end;

    theorem :: ANPROJ10:20

    

     Th13: (P,Q,R) are_collinear & P <> R & Q <> R implies ( affine-ratio (R,P,Q)) = (1 / (1 - ( affine-ratio (P,Q,R))))

    proof

      assume that

       A1: (P,Q,R) are_collinear and

       A2: P <> R and

       A3: Q <> R;

      set r = ( affine-ratio (P,Q,R)), s = ( affine-ratio (R,P,Q));

      

       A4: (1 - r) <> 0 by A1, A2, A3, Th07;

      

       A5: (r * (R - P)) = ((Q + ( 0. V)) - P) by A1, A2, Def02

      .= ((Q + (( - R) + R)) - P) by RLVECT_1: 5

      .= (((Q - R) + R) - P) by RLVECT_1:def 3

      .= ((Q - R) + ( - ( - (R - P)))) by RLVECT_1:def 3

      .= ((Q - R) - (P - R)) by RLVECT_1: 33;

      

       A6: (R,P,Q) are_collinear by A1;

      

      then ( - (s * (Q - R))) = ( - (P - R)) by A3, Def02

      .= (R - P) by RLVECT_1: 33;

      

      then

       A7: (R - P) = (( - 1) * (s * (Q - R))) by RLVECT_1: 16

      .= ((( - 1) * s) * (Q - R)) by RLVECT_1:def 7

      .= (( - s) * (Q - R));

      (r * (R - P)) = ((Q - R) + ( - (s * (Q - R)))) by A5, A6, A3, Def02

      .= ((Q - R) + (( - 1) * (s * (Q - R)))) by RLVECT_1: 16

      .= ((Q - R) + ((( - 1) * s) * (Q - R))) by RLVECT_1:def 7

      .= ((1 * (Q - R)) + (( - s) * (Q - R))) by RLVECT_1:def 8

      .= ((1 - s) * (Q - R)) by RLVECT_1:def 6;

      then ((r * ( - s)) * (Q - R)) = ((1 - s) * (Q - R)) by A7, RLVECT_1:def 7;

      then ( - (r * s)) = (1 - s) by Th08, A3;

      then (s * (1 - r)) = 1;

      hence thesis by A4, XCMPLX_1: 89;

    end;

    theorem :: ANPROJ10:21

    for r be Real st (P,Q,R) are_collinear & P <> R & Q <> R & P <> Q & r = ( affine-ratio (P,Q,R)) holds ( affine-ratio (P,R,Q)) = (1 / r) & ( affine-ratio (Q,P,R)) = (r / (r - 1)) & ( affine-ratio (Q,R,P)) = ((r - 1) / r) & ( affine-ratio (R,P,Q)) = (1 / (1 - r)) & ( affine-ratio (R,Q,P)) = (1 - r) by Th09, Th10, Th11, Th12, Th13;

    theorem :: ANPROJ10:22

    for a be non zero Real st (P,Q,R) are_collinear & P <> R holds ( affine-ratio (P,Q,R)) = ( affine-ratio ((a * P),(a * Q),(a * R)))

    proof

      let a be non zero Real;

      assume

       A1: (P,Q,R) are_collinear & P <> R;

      reconsider aP = (a * P), aQ = (a * Q), aR = (a * R) as Element of V;

      now

        thus aP <> aR by A1, RLVECT_1: 36;

        Q in ( Line (P,R)) by A1, RLTOPSP1: 80;

        then Q in the set of all (((1 - l) * P) + (l * R)) where l be Real by RLTOPSP1:def 14;

        then

        consider l be Real such that

         A2: Q = (((1 - l) * P) + (l * R));

        reconsider aL = ( Line (aP,aR)) as line of V;

        

         H1: aP in aL & aR in aL by RLTOPSP1: 72;

        aQ = ((a * ((1 - l) * P)) + (a * (l * R))) by A2, RLVECT_1:def 5

        .= (((a * (1 - l)) * P) + (a * (l * R))) by RLVECT_1:def 7

        .= (((a * (1 - l)) * P) + ((a * l) * R)) by RLVECT_1:def 7

        .= (((1 - l) * (a * P)) + ((a * l) * R)) by RLVECT_1:def 7

        .= (((1 - l) * aP) + (l * aR)) by RLVECT_1:def 7;

        then aQ in the set of all (((1 - l) * aP) + (l * aR)) where l be Real;

        then aQ in aL by RLTOPSP1:def 14;

        hence (aP,aQ,aR) are_collinear by H1;

      end;

      then (aQ - aP) = (( affine-ratio (aP,aQ,aR)) * (aR - aP)) by Def02;

      then (a * (Q - P)) = (( affine-ratio (aP,aQ,aR)) * (aR - aP)) by RLVECT_1: 34;

      then (a * (Q - P)) = (( affine-ratio (aP,aQ,aR)) * (a * (R - P))) by RLVECT_1: 34;

      then (a * (Q - P)) = ((( affine-ratio (aP,aQ,aR)) * a) * (R - P)) by RLVECT_1:def 7;

      then (a * (Q - P)) = (a * (( affine-ratio (aP,aQ,aR)) * (R - P))) by RLVECT_1:def 7;

      then (Q - P) = (( affine-ratio (aP,aQ,aR)) * (R - P)) by RLVECT_1: 36;

      hence thesis by A1, Def02;

    end;

    theorem :: ANPROJ10:23

    for x,y be Element of ( REAL 1) holds for p,q be Tuple of 1, REAL st p = x & q = y holds (x + y) = (p + q);

    theorem :: ANPROJ10:24

    for x,y be Element of ( TOP-REAL 1) holds for p,q be Tuple of 1, REAL st p = x & q = y holds (x + y) = (p + q);

    theorem :: ANPROJ10:25

    for x,y be Element of ( TOP-REAL 1) holds for p,q be Tuple of 1, REAL st p = x & q = y holds (x - y) = (p - q);

    theorem :: ANPROJ10:26

    for x be Element of ( TOP-REAL 1) holds for p be Tuple of 1, REAL st p = x holds ( - x) = ( - p);

    theorem :: ANPROJ10:27

    

     Th14: for T be RealLinearSpace holds for x,y be Element of T holds for p,q be Tuple of 1, REAL st T = ( TOP-REAL 1) & p = x & q = y holds (x + y) = (p + q)

    proof

      let T be RealLinearSpace;

      let x,y be Element of T;

      let p,q be Tuple of 1, REAL ;

      assume that

       A1: T = ( TOP-REAL 1) and

       A2: p = x and

       A3: q = y;

      

       A4: p in ( Funcs (( Seg 1), REAL )) & q is Element of ( Funcs (( Seg 1), REAL )) by SRINGS_5: 11;

      (the addF of the RLSStruct of ( TOP-REAL 1) . (p,q)) = (the addF of ( RealVectSpace ( Seg 1)) . (p,q)) by EUCLID:def 8

      .= (p + q) by A4, FUNCSDOM:def 1;

      hence thesis by A1, A2, A3, ALGSTR_0:def 1;

    end;

    theorem :: ANPROJ10:28

    

     Th15: for p be Tuple of 1, REAL holds ( - p) is Tuple of 1, REAL

    proof

      let p be Tuple of 1, REAL ;

      consider d be Element of REAL such that

       A1: p = <*d*> by FINSEQ_2: 97;

      ( - p) = <*( - d)*> by A1, RVSUM_1: 20;

      hence thesis;

    end;

    theorem :: ANPROJ10:29

    

     Th16: for T be RealLinearSpace holds for x be Element of T holds for p be Tuple of 1, REAL st T = ( TOP-REAL 1) & p = x holds ( - p) = ( - x)

    proof

      let T be RealLinearSpace;

      let x be Element of T;

      let p be Tuple of 1, REAL ;

      assume that

       A1: T = ( TOP-REAL 1) and

       A2: p = x;

      consider d be Element of REAL such that

       A3: p = <*d*> by FINSEQ_2: 97;

      reconsider x9 = <*( - d)*> as Tuple of 1, REAL ;

      reconsider n = 1 as Nat;

       REAL is non empty & REAL c= REAL ;

      then

      reconsider p9 = p as Element of (1 -tuples_on REAL ) by FINSEQ_2: 109;

      

       A4: the RLSStruct of ( TOP-REAL 1) = ( RealVectSpace ( Seg 1)) & ( 0.REAL 1) = <* 0 *> by EUCLID:def 8, FINSEQ_2: 59;

      

       A5: (p + ( - p)) = (p9 + ( - p9))

      .= ( 0. ( TOP-REAL 1)) by A4, RVSUM_1: 22;

       the TopStruct of ( TOP-REAL 1) = ( TopSpaceMetr ( Euclid 1)) by EUCLID:def 8;

      then

      reconsider x99 = x9 as Element of T by A1;

      

       A6: ( - p) = <*( - d)*> by A3, RVSUM_1: 20;

      (x + x99) = ( 0. T) by A1, A2, A6, Th14, A5;

      then ( - x) = x99 by RLVECT_1:def 10;

      hence thesis by A3, RVSUM_1: 20;

    end;

    theorem :: ANPROJ10:30

    

     Th17: for T be RealLinearSpace holds for x be Element of T holds for p be Element of ( TOP-REAL 1) st T = ( TOP-REAL 1) & p = x holds ( - p) = ( - x)

    proof

      let T be RealLinearSpace;

      let x be Element of T;

      let p be Element of ( TOP-REAL 1);

      assume that

       A1: T = ( TOP-REAL 1) and

       A2: p = x;

      p is Element of ( REAL 1) by EUCLID: 22;

      then

      reconsider p9 = p as Tuple of 1, REAL ;

      ( - p9) = ( - x) by A1, A2, Th16;

      hence thesis;

    end;

    theorem :: ANPROJ10:31

    

     Th18: for T be RealLinearSpace holds for x,y be Element of T holds for p,q be Tuple of 1, REAL st T = ( TOP-REAL 1) & p = x & q = y holds (x - y) = (p - q)

    proof

      let T be RealLinearSpace;

      let x,y be Element of T;

      let p,q be Tuple of 1, REAL ;

      assume that

       A1: T = ( TOP-REAL 1) and

       A2: p = x and

       A3: q = y;

      set p9 = p, q9 = q;

      reconsider y9 = ( - y) as Element of T;

      reconsider qm9 = ( - q) as Tuple of 1, REAL by Th15;

      

       A4: p9 in ( Funcs (( Seg 1), REAL )) & qm9 is Element of ( Funcs (( Seg 1), REAL )) by SRINGS_5: 11;

      

       A5: (the addF of the RLSStruct of ( TOP-REAL 1) . (p9,qm9)) = (the addF of ( RealVectSpace ( Seg 1)) . (p9,qm9)) by EUCLID:def 8

      .= (p9 + qm9) by A4, FUNCSDOM:def 1;

      (x - y) = (the addF of ( TOP-REAL 1) . (x,( - y))) by A1, ALGSTR_0:def 1

      .= (p - q) by A5, A1, A2, A3, Th16;

      hence thesis;

    end;

    theorem :: ANPROJ10:32

    

     Th19: for T be RealLinearSpace holds for x,y be Element of T holds for p,q be Element of ( TOP-REAL 1) st T = ( TOP-REAL 1) & p = x & q = y holds (x + y) = (p + q)

    proof

      let T be RealLinearSpace;

      let x,y be Element of T;

      let p,q be Element of ( TOP-REAL 1);

      assume that

       A1: T = ( TOP-REAL 1) and

       A2: p = x and

       A3: q = y;

      reconsider p9 = p, q9 = q as Element of ( REAL 1) by EUCLID: 22;

      (x + y) = (p9 + q9) by A1, A2, A3, Th14;

      hence thesis;

    end;

    theorem :: ANPROJ10:33

    

     Th20: for D be set holds for d be Element of D holds (( Seg 1) --> d) = <*d*>

    proof

      let D be set;

      let d be Element of D;

      (( Seg 1) --> d) = (1 |-> d)

      .= <*d*> by FINSEQ_2: 59;

      hence thesis;

    end;

    theorem :: ANPROJ10:34

    

     Th21: for a,r be Real holds ( multreal .: ((( Seg 1) --> a), <*r*>)) = <*(a * r)*>

    proof

      let a,r be Real;

      reconsider r1 = a, r2 = r as Element of REAL by XREAL_0:def 1;

      a is Element of REAL by XREAL_0:def 1;

      

      then ( multreal .: ((( Seg 1) --> a), <*r*>)) = ( multreal .: ( <*a*>, <*r*>)) by Th20

      .= <*( multreal . (r1,r2))*> by FINSEQ_2: 74

      .= <*(r1 * r2)*> by BINOP_2:def 11;

      hence thesis;

    end;

    theorem :: ANPROJ10:35

    

     Th22: for a be Real holds for p be Tuple of 1, REAL holds ( multreal .: ((( dom p) --> a),p)) = (a * p)

    proof

      let a be Real;

      let p be Tuple of 1, REAL ;

      consider d be Element of REAL such that

       A1: p = <*d*> by FINSEQ_2: 97;

      

       A2: (a * p) = <*(a * d)*> by A1, RVSUM_1: 47;

      ( dom p) = ( Seg 1) by A1, FINSEQ_1:def 8;

      hence thesis by A1, A2, Th21;

    end;

    theorem :: ANPROJ10:36

    for a be Real holds for p be Tuple of 1, REAL holds ( multreal .: ((( dom p) --> a),p)) = (a * p) by Th22;

    theorem :: ANPROJ10:37

    

     Th23: for T be RealLinearSpace holds for x,y be Element of T holds for a be Real holds for p,q be Tuple of 1, REAL st T = ( TOP-REAL 1) & p = x & q = y & x = (a * y) holds p = (a * q)

    proof

      let T be RealLinearSpace;

      let x,y be Element of T;

      let a be Real;

      let p,q be Tuple of 1, REAL ;

      assume that

       A1: T = ( TOP-REAL 1) and

       A2: p = x and

       A3: q = y and

       A4: x = (a * y);

      set p9 = q;

      

       A5: p9 in ( Funcs (( Seg 1), REAL )) by SRINGS_5: 11;

      (the Mult of the RLSStruct of ( TOP-REAL 1) . (a,p9)) = (the Mult of ( RealVectSpace ( Seg 1)) . (a,p9)) by EUCLID:def 8

      .= ( multreal [;] (a,p9)) by A5, FUNCSDOM:def 3

      .= ( multreal .: ((( dom p9) --> a),p9)) by FUNCOP_1: 31

      .= (a * p9) by Th22;

      hence thesis by A1, A2, A3, A4;

    end;

    theorem :: ANPROJ10:38

    for T be RealLinearSpace holds for x,y be Element of T holds for a be Real holds for p,q be Element of ( TOP-REAL 1) st T = ( TOP-REAL 1) & p = x & q = y holds x = (a * y) implies p = (a * q)

    proof

      let T be RealLinearSpace;

      let x,y be Element of T;

      let a be Real;

      let p,q be Element of ( TOP-REAL 1);

      assume that

       A1: T = ( TOP-REAL 1) and

       A2: p = x and

       A3: q = y and

       A4: x = (a * y);

      p is Element of ( REAL 1) & q is Element of ( REAL 1) by EUCLID: 22;

      then

      reconsider p9 = p, q9 = q as Tuple of 1, REAL ;

      p9 = (a * q9) by A1, A2, A3, A4, Th23;

      hence thesis;

    end;

    theorem :: ANPROJ10:39

    for T be RealLinearSpace holds for x,y be Element of T holds for p,q be Element of ( TOP-REAL 1) st T = ( TOP-REAL 1) & p = x & q = y holds (x - y) = (p - q)

    proof

      let T be RealLinearSpace;

      let x,y be Element of T;

      let p,q be Element of ( TOP-REAL 1);

      assume that

       A1: T = ( TOP-REAL 1) and

       A2: p = x and

       A3: q = y;

      reconsider y9 = ( - y) as Element of T;

      reconsider q as Element of ( REAL 1) by EUCLID: 22;

      reconsider q9 = ( - q) as Element of ( TOP-REAL 1) by EUCLID: 22;

      ( - q) = ( - y) by A1, A3, Th17;

      hence thesis by A1, A2, Th19;

    end;

    theorem :: ANPROJ10:40

    

     Th24: for p,q be Tuple of 1, REAL holds for r be Real st p = (r * q) & p <> <* 0 *> holds ex a,b be Real st p = <*a*> & q = <*b*> & r = (a / b)

    proof

      let p,q be Tuple of 1, REAL ;

      let r be Real;

      assume that

       A1: p = (r * q) and

       A2: p <> <* 0 *>;

      consider r1 be Element of REAL such that

       A3: p = <*r1*> by FINSEQ_2: 97;

      consider r2 be Element of REAL such that

       A4: q = <*r2*> by FINSEQ_2: 97;

      reconsider r1, r2 as Real;

      take r1, r2;

      

       A5: <*r1*> = <*(r * r2)*> by A1, A3, A4, RVSUM_1: 47;

      then

       A6: r1 = (r * r2) by FINSEQ_1: 76;

      per cases ;

        suppose r2 = 0 ;

        hence thesis by A5, A2, A3;

      end;

        suppose

         A7: r2 <> 0 ;

        r = (r * 1)

        .= (r * (r2 / r2)) by A7, XCMPLX_1: 60

        .= (r1 / r2) by A6;

        hence thesis by A3, A4;

      end;

    end;

    theorem :: ANPROJ10:41

    

     Th25: for x,y,z be Element of ( TOP-REAL 1) holds (x,y,z) are_collinear

    proof

      let x,y,z be Element of ( TOP-REAL 1);

      per cases ;

        suppose

         A1: z <> y;

        reconsider L = ( Line (y,z)) as line of ( TOP-REAL 1);

        

         H1: y in L & z in L by RLTOPSP1: 72;

        reconsider x1 = x, y1 = y, z1 = z as Element of ( REAL 1) by EUCLID: 22;

        

         A2: x1 in ( REAL 1) & y1 in ( REAL 1) & z1 in ( REAL 1);

        consider xr be Element of REAL such that

         A3: x = <*xr*> by A2, FINSEQ_2: 97;

        consider yr be Element of REAL such that

         A4: y = <*yr*> by A2, FINSEQ_2: 97;

        consider zr be Element of REAL such that

         A5: z = <*zr*> by A2, FINSEQ_2: 97;

        

         A6: (zr - yr) <> 0 by A4, A5, A1;

        reconsider r = ((xr - yr) / (zr - yr)) as Real;

        

         A7: (((1 - r) * yr) + (r * zr)) = (yr + (((xr - yr) / (zr - yr)) * (zr - yr)))

        .= (yr + (xr - yr)) by A6, XCMPLX_1: 87

        .= xr;

        (((1 - r) * y1) + (r * z1)) = ( <*((1 - r) * yr)*> + (r * <*zr*>)) by A4, A5, RVSUM_1: 47

        .= ( <*((1 - r) * yr)*> + <*(r * zr)*>) by RVSUM_1: 47

        .= x by RVSUM_1: 13, A3, A7;

        then x in the set of all (((1 - r) * y1) + (r * z1)) where r be Real;

        then x in ( Line (y1,z1)) by EUCLID_4:def 1;

        then x in L by EUCLID12: 4;

        hence thesis by H1;

      end;

        suppose z = y;

        then x in ( Line (x,y)) & y in ( Line (x,y)) & z in ( Line (x,y)) by RLTOPSP1: 72;

        hence thesis;

      end;

    end;

    theorem :: ANPROJ10:42

    for T be RealLinearSpace st T = ( TOP-REAL 1) holds for x,y,z be Element of T holds (x,y,z) are_collinear by Th25;

    theorem :: ANPROJ10:43

    

     Th26: for T be RealLinearSpace st T = ( TOP-REAL 1) holds for x,y,z be Element of T st z <> x & y <> x holds ex a,b,c be Real st x = <*a*> & y = <*b*> & z = <*c*> & ( affine-ratio (x,y,z)) = ((b - a) / (c - a))

    proof

      let T be RealLinearSpace;

      assume

       A1: T = ( TOP-REAL 1);

      let x,y,z be Element of T;

      assume that

       A2: z <> x and

       A3: y <> x;

      reconsider p9 = x, q9 = y, r9 = z as Element of ( REAL 1) by A1, EUCLID: 22;

      reconsider p = p9, q = q9, r = r9 as Tuple of 1, REAL ;

      set ma = ( affine-ratio (x,y,z));

      reconsider yx = (y - x), zx = (z - x) as Element of T;

      (q9 - p9) is Element of (1 -tuples_on REAL ) & (r9 - p9) is Element of (1 -tuples_on REAL );

      then

      reconsider qp = (q - p), rp = (r - p) as Tuple of 1, REAL ;

      

       A4: qp = yx & rp = zx by A1, Th18;

      consider r1 be Element of REAL such that

       A5: q = <*r1*> by FINSEQ_2: 97;

      consider r2 be Element of REAL such that

       A6: p = <*r2*> by FINSEQ_2: 97;

      consider r3 be Element of REAL such that

       A7: r = <*r3*> by FINSEQ_2: 97;

      

       A8: qp = <*(r1 - r2)*> & rp = <*(r3 - r2)*> by A5, A6, A7, RVSUM_1: 29;

      now

        (x,y,z) are_collinear by A1, Th25;

        then (y - x) = (ma * (z - x)) by A2, Def02;

        hence qp = (ma * rp) by A4, A1, Th23;

        thus qp <> <* 0 *>

        proof

          assume qp = <* 0 *>;

          then (r1 - r2) = 0 by A8, FINSEQ_1: 76;

          hence contradiction by A5, A6, A3;

        end;

      end;

      then

      consider a,b be Real such that

       A9: qp = <*a*> and

       A10: rp = <*b*> and

       A11: ma = (a / b) by Th24;

      reconsider s1 = (r1 - r2), s2 = (r3 - r2) as Real;

      

       A12: a = s1 & b = s2 by A9, A10, A8, FINSEQ_1: 76;

      reconsider r2, r1, r3 as Real;

      take r2, r1, r3;

      thus thesis by A11, A12, A5, A6, A7;

    end;

    theorem :: ANPROJ10:44

    

     Th27: for x be Element of ( TOP-REAL 1) holds for a,r be Real st x = <*a*> holds (r * x) = <*(r * a)*>

    proof

      let x be Element of ( TOP-REAL 1);

      let a,r be Real;

      assume x = <*a*>;

      then

       A1: (x . 1) = a by FINSEQ_1:def 8;

      reconsider x9 = x as Element of ( REAL 1) by EUCLID: 22;

      

       A2: ((r * x9) . 1) = (r * (x . 1)) by RVSUM_1: 44;

      (r * x9) in ( REAL 1);

      then (r * x) is Element of ( TOP-REAL 1) by EUCLID: 22;

      then

      consider b be Real such that

       A3: (r * x) = <*b*> by JORDAN2B: 20;

      thus thesis by A1, A3, A2, FINSEQ_1:def 8;

    end;

    theorem :: ANPROJ10:45

    for x,y be Element of ( TOP-REAL 1) holds for a,b,r be Real st x = <*a*> & y = <*b*> holds x = (r * y) iff a = (r * b)

    proof

      let x,y be Element of ( TOP-REAL 1);

      let a,b,r be Real;

      assume that

       A1: x = <*a*> and

       A2: y = <*b*>;

      reconsider rb = (r * b) as Real;

      hereby

        assume x = (r * y);

        then x = <*rb*> by A2, Th27;

        hence a = (r * b) by A1, FINSEQ_1: 76;

      end;

      assume a = (r * b);

      hence x = (r * y) by A2, A1, Th27;

    end;

    theorem :: ANPROJ10:46

    for x,y be Element of ( TOP-REAL 1) holds for a,b be Real st x = <*a*> & y = <*b*> holds (x - y) = <*(a - b)*> by RVSUM_1: 29;

    theorem :: ANPROJ10:47

    for V be RealLinearSpace holds for x,y be Element of F_Real holds for x9,y9 be Element of V st V = F_Real & x = x9 & y = y9 holds (x + y) = (x9 + y9);

    theorem :: ANPROJ10:48

    for V be RealLinearSpace holds for P,Q,R be Element of V st (P,Q,R) are_collinear & P <> R & Q <> R & P <> Q holds ( affine-ratio (P,Q,R)) <> 0 & ( affine-ratio (P,Q,R)) <> 1 by Th06, Th07;

    theorem :: ANPROJ10:49

    

     Th28: for V be RealLinearSpace holds for P,Q,R be Element of V st (P,Q,R) are_collinear & P <> R & Q <> R & P <> Q holds ex r be non unit non zero Real st r = ( affine-ratio (P,Q,R)) & ( affine-ratio (P,R,Q)) = ( op1 r) & ( affine-ratio (Q,P,R)) = ( op1 ( op2 ( op1 r))) & ( affine-ratio (Q,R,P)) = ( op2 ( op1 r)) & ( affine-ratio (R,P,Q)) = ( op1 ( op2 r)) & ( affine-ratio (R,Q,P)) = ( op2 r)

    proof

      let V be RealLinearSpace;

      let P,Q,R be Element of V;

      assume that

       A1: (P,Q,R) are_collinear and

       A2: P <> R and

       A3: Q <> R and

       A4: P <> Q;

      

       A5: ( affine-ratio (P,Q,R)) <> 0 & ( affine-ratio (P,Q,R)) <> 1 by A1, A2, A3, A4, Th06, Th07;

      reconsider r = ( affine-ratio (P,Q,R)) as Element of REAL by XREAL_0:def 1;

      reconsider r9 = r as non unit non zero Real by A5, Def01;

      take r9;

      ( affine-ratio (P,R,Q)) = (1 / r) & ( affine-ratio (Q,P,R)) = (r / (r - 1)) & ( affine-ratio (Q,R,P)) = ((r - 1) / r) & ( affine-ratio (R,P,Q)) = (1 / (1 - r)) & ( affine-ratio (R,Q,P)) = (1 - r) by A1, A2, A3, A4, Th09, Th10, Th11, Th12, Th13;

      hence thesis by Th01;

    end;

    begin

    theorem :: ANPROJ10:50

    for X be non empty set holds for x be Tuple of 4, X holds for P,Q,R,S be Element of X st x = <*P, Q, R, S*> holds ( pi_1234 x) = <*P, Q, R, S*> & ( pi_1243 x) = <*P, Q, S, R*> & ( pi_1324 x) = <*P, R, Q, S*> & ( pi_1342 x) = <*P, R, S, Q*> & ( pi_1423 x) = <*P, S, Q, R*> & ( pi_1432 x) = <*P, S, R, Q*> & ( pi_2134 x) = <*Q, P, R, S*> & ( pi_2143 x) = <*Q, P, S, R*> & ( pi_2314 x) = <*Q, R, P, S*> & ( pi_2341 x) = <*Q, R, S, P*> & ( pi_2413 x) = <*Q, S, P, R*> & ( pi_2431 x) = <*Q, S, R, P*> & ( pi_3124 x) = <*R, P, Q, S*> & ( pi_3142 x) = <*R, P, S, Q*> & ( pi_3214 x) = <*R, Q, P, S*> & ( pi_3241 x) = <*R, Q, S, P*> & ( pi_3412 x) = <*R, S, P, Q*> & ( pi_3421 x) = <*R, S, Q, P*> & ( pi_4123 x) = <*S, P, Q, R*> & ( pi_4132 x) = <*S, P, R, Q*> & ( pi_4213 x) = <*S, Q, P, R*> & ( pi_4231 x) = <*S, Q, R, P*> & ( pi_4312 x) = <*S, R, P, Q*> & ( pi_4321 x) = <*S, R, Q, P*>;

    theorem :: ANPROJ10:51

    for X be non empty set holds for x be Tuple of 4, X holds ( pi_1324 ( pi_1243 x)) = ( pi_1423 x) & ( pi_2143 ( pi_1243 x)) = ( pi_2134 x) & ( pi_3412 ( pi_1243 x)) = ( pi_4312 x) & ( pi_4321 ( pi_1243 x)) = ( pi_3421 x) & ( pi_3412 ( pi_1324 x)) = ( pi_2413 x) & ( pi_2143 ( pi_1324 x)) = ( pi_3142 x) & ( pi_4321 ( pi_1324 x)) = ( pi_4231 x) & ( pi_3412 ( pi_1423 x)) = ( pi_2314 x) & ( pi_2143 ( pi_1423 x)) = ( pi_4132 x) & ( pi_4321 ( pi_1423 x)) = ( pi_3241 x) & ( pi_1243 ( pi_1423 x)) = ( pi_1432 x) & ( pi_4321 ( pi_1432 x)) = ( pi_2341 x) & ( pi_3412 ( pi_1432 x)) = ( pi_3214 x) & ( pi_2143 ( pi_1432 x)) = ( pi_4123 x) & ( pi_4321 ( pi_3124 x)) = ( pi_4213 x) & ( pi_3412 ( pi_3124 x)) = ( pi_2431 x) & ( pi_2143 ( pi_3124 x)) = ( pi_1342 x) & ( pi_4312 ( pi_3124 x)) = ( pi_4231 x) & ( pi_4321 ( pi_3124 x)) = ( pi_4213 x);

    reserve x for Tuple of 4, the carrier of V,

P9,Q9,R9,S9 for Element of V;

    definition

      let V be RealLinearSpace;

      let P,Q,R,S be Element of V;

      :: ANPROJ10:def29

      func cross-ratio (P,Q,R,S) -> Real equals (( affine-ratio (R,P,Q)) / ( affine-ratio (S,P,Q)));

      coherence ;

    end

    theorem :: ANPROJ10:52

    

     Th31: (P,Q,R,S) are_collinear & R <> Q & S <> Q & S <> P implies (R = P iff ( cross-ratio (P,Q,R,S)) = 0 )

    proof

      assume that

       A1: (P,Q,R,S) are_collinear and

       A2: R <> Q and

       A3: S <> Q and

       A4: S <> P;

      consider L be line of V such that

       A5: P in L & Q in L & R in L & S in L by A1;

      

       A6: (R,P,Q) are_collinear & (S,P,Q) are_collinear by A5;

      hereby

        assume R = P;

        then ( affine-ratio (R,P,Q)) = 0 by A6, A2, Th06;

        hence ( cross-ratio (P,Q,R,S)) = 0 ;

      end;

      assume

       A7: ( cross-ratio (P,Q,R,S)) = 0 ;

      per cases ;

        suppose ( affine-ratio (S,P,Q)) = 0 ;

        hence R = P by A3, A4, A6, Th06;

      end;

        suppose ( affine-ratio (S,P,Q)) <> 0 ;

        then ( affine-ratio (R,P,Q)) = 0 by A7;

        hence R = P by A2, A6, Th06;

      end;

    end;

    theorem :: ANPROJ10:53

    P <> R & P <> S implies ( cross-ratio (P,P,R,S)) = 1

    proof

      assume that

       A1: P <> R and

       A2: P <> S;

      (R,P,P) are_collinear & (S,P,P) are_collinear by Th05;

      then ( affine-ratio (R,P,P)) = 1 & ( affine-ratio (S,P,P)) = 1 by A1, A2, Th07;

      hence thesis;

    end;

    theorem :: ANPROJ10:54

    

     Th32: (P,Q,R,S) are_collinear & R <> Q & S <> Q & R <> S & ( cross-ratio (P,Q,R,S)) = 1 implies P = Q

    proof

      assume that

       A1: (P,Q,R,S) are_collinear and

       A2: R <> Q and

       A3: S <> Q and

       A4: R <> S and

       A5: ( cross-ratio (P,Q,R,S)) = 1;

      

       A6: ( affine-ratio (R,P,Q)) = ( affine-ratio (S,P,Q)) by A5, XCMPLX_1: 58;

      set r = ( affine-ratio (R,P,Q));

      

       A7: (R,P,Q) are_collinear & (S,P,Q) are_collinear by A1;

      then ((P + ( 0. V)) - R) = (r * ((Q + ( 0. V)) - R)) by A2, Def02;

      

      then ((P + (( - S) + S)) - R) = (r * ((Q + ( 0. V)) - R)) by RLVECT_1: 5

      .= (r * ((Q + (( - S) + S)) - R)) by RLVECT_1: 5

      .= (r * (((Q - S) + S) - R)) by RLVECT_1:def 3;

      

      then (((P - S) + S) - R) = (r * (((Q - S) + S) - R)) by RLVECT_1:def 3

      .= (r * ((Q - S) + (S - R))) by RLVECT_1:def 3

      .= ((r * (Q - S)) + (r * (S - R))) by RLVECT_1:def 5

      .= ((P - S) + (r * (S - R))) by A7, A6, A3, Def02;

      then (( - (P - S)) + ((P - S) + (S - R))) = (( - (P - S)) + ((P - S) + (r * (S - R)))) by RLVECT_1:def 3;

      

      then ((( - (P - S)) + (P - S)) + (S - R)) = (( - (P - S)) + ((P - S) + (r * (S - R)))) by RLVECT_1:def 3

      .= ((( - (P - S)) + (P - S)) + (r * (S - R))) by RLVECT_1:def 3;

      

      then (r * (S - R)) = (S - R) by RLVECT_1: 8

      .= (1 * (S - R)) by RLVECT_1:def 8;

      then r = 1 by A4, Th08;

      hence P = Q by A2, Th07, A7;

    end;

    theorem :: ANPROJ10:55

    (P,Q,R,S) are_collinear & (P9,Q9,R9,S9) are_collinear & S <> P & S <> Q & S9 <> P9 & S9 <> Q9 implies (( cross-ratio (P,Q,R,S)) = ( cross-ratio (P9,Q9,R9,S9)) iff (( affine-ratio (R,P,Q)) * ( affine-ratio (S9,P9,Q9))) = (( affine-ratio (R9,P9,Q9)) * ( affine-ratio (S,P,Q))))

    proof

      assume that

       A1: (P,Q,R,S) are_collinear and

       A2: (P9,Q9,R9,S9) are_collinear and

       A3: S <> P and

       A4: S <> Q and

       A5: S9 <> P9 and

       A6: S9 <> Q9;

      set r = ( affine-ratio (R,P,Q)), s = ( affine-ratio (S,P,Q)), r9 = ( affine-ratio (R9,P9,Q9)), s9 = ( affine-ratio (S9,P9,Q9));

      (S,P,Q) are_collinear & (S9,P9,Q9) are_collinear by A1, A2;

      then s <> 0 & s9 <> 0 by A3, A4, A5, A6, Th06;

      hence thesis by XCMPLX_1: 94, XCMPLX_1: 95;

    end;

    

     Lm02: for r be Real st (P - Q) = (r * (R - S)) holds (Q - P) = (r * (S - R))

    proof

      let r be Real;

      assume

       A1: (P - Q) = (r * (R - S));

      (Q - P) = ( - (r * (R - S))) by A1, RLVECT_1: 33

      .= (r * ( - (R - S))) by RLVECT_1: 25

      .= (r * (S - R)) by RLVECT_1: 33;

      hence thesis;

    end;

    theorem :: ANPROJ10:56

    

     Th33: (P,Q,R,S) are_collinear & P <> S & R <> Q & S <> Q implies ( cross-ratio (P,Q,R,S)) = ( cross-ratio (R,S,P,Q))

    proof

      assume that

       A1: (P,Q,R,S) are_collinear and

       A2: P <> S and

       A3: R <> Q and

       A4: S <> Q;

      

       A5: (R,P,Q) are_collinear & (P,R,S) are_collinear & (S,P,Q) are_collinear & (Q,R,S) are_collinear by A1;

      set r1 = ( affine-ratio (R,P,Q)), r2 = ( affine-ratio (S,P,Q)), s1 = ( affine-ratio (P,R,S)), s2 = ( affine-ratio (Q,R,S));

      

       A6: r2 <> 0 & s2 <> 0 by A2, A3, A4, A5, Th06;

      

       A7: (Q - S) <> ( 0. V) by A4, RLVECT_1: 21;

      

       A8: (P - R) = (r1 * (Q - R)) by A5, A3, Def02;

      

       A9: (P - S) = (r2 * (Q - S)) by A5, A4, Def02;

      (R - Q) = (s2 * (S - Q)) by A5, A4, Def02;

      then

       A10: (Q - R) = (s2 * (Q - S)) by Lm02;

      (R - P) = (s1 * (S - P)) by A5, A2, Def02;

      

      then (P - R) = (s1 * (P - S)) by Lm02

      .= ((s1 * r2) * (Q - S)) by A9, RLVECT_1:def 7;

      then ((r1 * s2) * (Q - S)) = ((s1 * r2) * (Q - S)) by A8, A10, RLVECT_1:def 7;

      hence thesis by A7, RLVECT_1: 37, A6, XCMPLX_1: 94;

    end;

    theorem :: ANPROJ10:57

    

     Th34: for V be RealLinearSpace holds for P,Q,R,S be Element of V st (P,Q,R,S) are_collinear & P <> R & P <> S & R <> Q & S <> Q holds ( cross-ratio (P,Q,R,S)) = ( cross-ratio (Q,P,S,R))

    proof

      let V be RealLinearSpace;

      let P,Q,R,S be Element of V;

      assume that

       A1: (P,Q,R,S) are_collinear and

       A2: P <> R and

       A3: P <> S and

       A4: R <> Q and

       A5: S <> Q;

      set r1 = ( affine-ratio (R,P,Q)), r2 = ( affine-ratio (S,P,Q)), s1 = ( affine-ratio (S,Q,P)), s2 = ( affine-ratio (R,Q,P));

      per cases ;

        suppose

         A6: P = Q;

        (R,P,P) are_collinear & (S,P,P) are_collinear by Th05;

        then r1 = 1 & r2 = 1 & s1 = 1 & s2 = 1 by A2, A3, A6, Th07;

        hence thesis;

      end;

        suppose

         A7: P <> Q;

        (P,Q,R) are_collinear by A1;

        then

        consider r9 be non unit non zero Real such that

         A8: r9 = ( affine-ratio (P,Q,R)) & ( affine-ratio (P,R,Q)) = ( op1 r9) & ( affine-ratio (Q,P,R)) = ( op1 ( op2 ( op1 r9))) & ( affine-ratio (Q,R,P)) = ( op2 ( op1 r9)) & ( affine-ratio (R,P,Q)) = ( op1 ( op2 r9)) & ( affine-ratio (R,Q,P)) = ( op2 r9) by A2, A4, A7, Th28;

        (P,Q,S) are_collinear & P <> S & Q <> S by A1, A3, A5;

        then ex s9 be non unit non zero Real st s9 = ( affine-ratio (P,Q,S)) & ( affine-ratio (P,S,Q)) = ( op1 s9) & ( affine-ratio (Q,P,S)) = ( op1 ( op2 ( op1 s9))) & ( affine-ratio (Q,S,P)) = ( op2 ( op1 s9)) & ( affine-ratio (S,P,Q)) = ( op1 ( op2 s9)) & ( affine-ratio (S,Q,P)) = ( op2 s9) by A7, Th28;

        hence thesis by A8;

      end;

    end;

    theorem :: ANPROJ10:58

    

     Th34bis: (P,Q,R,S) are_collinear & P <> R & P <> S & R <> Q & S <> Q implies ( cross-ratio (P,Q,R,S)) = ( cross-ratio (S,R,Q,P))

    proof

      assume that

       A1: (P,Q,R,S) are_collinear and

       A2: P <> R and

       A3: P <> S and

       A4: R <> Q and

       A5: S <> Q;

      (R,S,P,Q) are_collinear by A1;

      then ( cross-ratio (R,S,P,Q)) = ( cross-ratio (S,R,Q,P)) by A2, A3, A4, A5, Th34;

      hence thesis by A1, A3, A4, A5, Th33;

    end;

    theorem :: ANPROJ10:59

    ( cross-ratio (P,Q,S,R)) = (1 / ( cross-ratio (P,Q,R,S))) by XCMPLX_1: 57;

    theorem :: ANPROJ10:60

    (P,Q,R,S) are_collinear & P <> R & P <> S & R <> Q & S <> Q implies ( cross-ratio (Q,P,R,S)) = (1 / ( cross-ratio (P,Q,R,S)))

    proof

      assume that

       A1: (P,Q,R,S) are_collinear and

       A2: P <> R and

       A3: P <> S and

       A4: R <> Q and

       A5: S <> Q;

      

       A6: ( cross-ratio (P,Q,S,R)) = (1 / ( cross-ratio (P,Q,R,S))) by XCMPLX_1: 57;

      (Q,P,R,S) are_collinear & P <> R & P <> S & R <> Q & S <> Q by A2, A3, A4, A5, A1;

      hence thesis by A6, Th34;

    end;

    theorem :: ANPROJ10:61

    (P,Q,R,S) are_collinear & P <> R & P <> S & R <> Q & S <> Q implies ( cross-ratio (R,S,Q,P)) = (1 / ( cross-ratio (P,Q,R,S)))

    proof

      assume that

       A1: (P,Q,R,S) are_collinear and

       A2: P <> R and

       A3: P <> S and

       A4: R <> Q and

       A5: S <> Q;

      

       A6: ( cross-ratio (P,Q,S,R)) = (1 / ( cross-ratio (P,Q,R,S))) by XCMPLX_1: 57;

      (P,Q,S,R) are_collinear & P <> R & P <> S & R <> Q & S <> Q by A1, A2, A3, A4, A5;

      hence thesis by A6, Th34bis;

    end;

    theorem :: ANPROJ10:62

    (P,Q,R,S) are_collinear & P <> R & P <> S & R <> Q & S <> Q implies ( cross-ratio (S,R,P,Q)) = (1 / ( cross-ratio (P,Q,R,S)))

    proof

      assume that

       A1: (P,Q,R,S) are_collinear and

       A2: P <> R and

       A3: P <> S and

       A4: R <> Q and

       A5: S <> Q;

      

       A6: ( cross-ratio (P,Q,S,R)) = (1 / ( cross-ratio (P,Q,R,S))) by XCMPLX_1: 57;

      (S,R,P,Q) are_collinear & P <> R & P <> S & R <> Q & S <> Q by A1, A2, A3, A4, A5;

      hence thesis by A6, Th33;

    end;

    theorem :: ANPROJ10:63

    

     Th35: (P,Q,R,S) are_collinear & (P,Q,R,S) are_mutually_distinct implies ( cross-ratio (P,R,Q,S)) = (1 - ( cross-ratio (P,Q,R,S)))

    proof

      assume that

       A1: (P,Q,R,S) are_collinear and

       A2: (P,Q,R,S) are_mutually_distinct ;

      

       A3: P <> R & P <> S & R <> Q & S <> Q & S <> R & P <> Q by A2, ZFMISC_1:def 6;

      set r1 = ( affine-ratio (R,P,Q)), r2 = ( affine-ratio (S,P,Q)), s1 = ( affine-ratio (Q,P,R)), s2 = ( affine-ratio (S,P,R)), r = ( affine-ratio (P,Q,R));

      

       A4: (P,Q,R) are_collinear by A1;

      then

       A5: r1 = (1 / (1 - r)) & s1 = (r / (r - 1)) by A3, Th10, Th13;

      (P,Q,R) are_collinear by A1;

      then

       A6: (r - 1) <> 0 by A3, Th07;

      

       A7: (1 - s1) = r1

      proof

        (1 - s1) = (1 - (r / (r - 1))) by A4, A3, Th10

        .= (((r - 1) / (r - 1)) - (r / (r - 1))) by A6, XCMPLX_1: 60

        .= (( - 1) / (r - 1))

        .= (1 / ( - (r - 1))) by XCMPLX_1: 192;

        hence thesis by A5;

      end;

      R <> Q & (R,P,Q) are_collinear by A1, A2, ZFMISC_1:def 6;

      then

       A8: (r2 * (P - R)) = (r2 * (r1 * (Q - R))) by Def02;

      

       A9: S <> Q & (S,P,Q) are_collinear by A1, A2, ZFMISC_1:def 6;

      

       A10: S <> R & (S,P,R) are_collinear by A1, A2, ZFMISC_1:def 6;

      then

       A11: (P - S) = (s2 * (R - S)) by Def02;

      (S,P,Q) are_collinear by A1;

      then

       A12: r2 <> 0 by A3, Th06;

      (S,P,R) are_collinear by A1;

      then

       A13: s2 <> 0 by A3, Th06;

      (P - R) = ((P + ( 0. V)) - R)

      .= ((P + (( - S) + S)) - R) by RLVECT_1: 5

      .= (((P - S) + S) - R) by RLVECT_1:def 3

      .= ((P - S) + (S - R)) by RLVECT_1:def 3

      .= ((s2 * (R - S)) + (S - R)) by A10, Def02

      .= ((s2 * (R - S)) + ( - (R - S))) by RLVECT_1: 33

      .= ((s2 * (R - S)) + (( - 1) * (R - S))) by RLVECT_1: 16

      .= ((s2 - 1) * (R - S)) by RLVECT_1:def 6;

      then

       A14: (r2 * (P - R)) = ((r2 * (s2 - 1)) * (R - S)) by RLVECT_1:def 7;

      (r1 * (Q - R)) = (r1 * ((Q + ( 0. V)) - R))

      .= (r1 * ((Q + (( - S) + S)) - R)) by RLVECT_1: 5

      .= (r1 * (((Q - S) + S) - R)) by RLVECT_1:def 3

      .= (r1 * ((Q - S) + (S - R))) by RLVECT_1:def 3

      .= ((r1 * (Q - S)) + (r1 * (S - R))) by RLVECT_1:def 5

      .= ((r1 * (Q - S)) + (r1 * ( - (R - S)))) by RLVECT_1: 33

      .= ((r1 * (Q - S)) + (r1 * (( - 1) * (R - S)))) by RLVECT_1: 16

      .= ((r1 * (Q - S)) + ((r1 * ( - 1)) * (R - S))) by RLVECT_1:def 7

      .= ((r1 * (Q - S)) + (( - r1) * (R - S)));

      

      then (r2 * (r1 * (Q - R))) = ((r2 * (r1 * (Q - S))) + (r2 * (( - r1) * (R - S)))) by RLVECT_1:def 5

      .= (((r2 * r1) * (Q - S)) + (r2 * (( - r1) * (R - S)))) by RLVECT_1:def 7

      .= ((r1 * (r2 * (Q - S))) + (r2 * (( - r1) * (R - S)))) by RLVECT_1:def 7

      .= ((r1 * (s2 * (R - S))) + (r2 * (( - r1) * (R - S)))) by A9, Def02, A11

      .= (((r1 * s2) * (R - S)) + (r2 * (( - r1) * (R - S)))) by RLVECT_1:def 7

      .= (((r1 * s2) * (R - S)) + ((r2 * ( - r1)) * (R - S))) by RLVECT_1:def 7

      .= (((r1 * s2) + (r2 * ( - r1))) * (R - S)) by RLVECT_1:def 6;

      then (r2 * (s2 - 1)) = ((r1 * s2) + (r2 * ( - r1))) by A14, A8, A3, Th08;

      then ((r1 * r2) - r2) = ((r1 * s2) - (r2 * s2));

      then (( - s1) * r2) = ((r1 - r2) * s2) by A7;

      then (s1 * r2) = ((r2 - r1) * s2);

      

      then (s1 / s2) = ((r2 - r1) / r2) by A12, A13, XCMPLX_1: 94

      .= ((r2 / r2) - (r1 / r2))

      .= (1 - (r1 / r2)) by A12, XCMPLX_1: 60;

      hence thesis;

    end;

    theorem :: ANPROJ10:64

    (P,Q,R,S) are_collinear & (P,Q,R,S) are_mutually_distinct implies ( cross-ratio (Q,S,P,R)) = (1 - ( cross-ratio (P,Q,R,S)))

    proof

      assume that

       A1: (P,Q,R,S) are_collinear and

       A2: (P,Q,R,S) are_mutually_distinct ;

      

       A3: P <> R & P <> S & R <> Q & S <> Q & S <> R & P <> Q by A2, ZFMISC_1:def 6;

      (P,R,Q,S) are_collinear by A1;

      then ( cross-ratio (P,R,Q,S)) = ( cross-ratio (Q,S,P,R)) by A3, Th33;

      hence thesis by A1, A2, Th35;

    end;

    theorem :: ANPROJ10:65

    (P,Q,R,S) are_collinear & (P,Q,R,S) are_mutually_distinct implies ( cross-ratio (R,P,S,Q)) = (1 - ( cross-ratio (P,Q,R,S)))

    proof

      assume that

       A1: (P,Q,R,S) are_collinear and

       A2: (P,Q,R,S) are_mutually_distinct ;

      

       A3: P <> R & P <> S & R <> Q & S <> Q & S <> R & P <> Q by A2, ZFMISC_1:def 6;

      (P,R,Q,S) are_collinear by A1;

      then ( cross-ratio (P,R,Q,S)) = ( cross-ratio (R,P,S,Q)) by A3, Th34;

      hence thesis by A1, A2, Th35;

    end;

    theorem :: ANPROJ10:66

    (P,Q,R,S) are_collinear & (P,Q,R,S) are_mutually_distinct implies ( cross-ratio (S,Q,R,P)) = (1 - ( cross-ratio (P,Q,R,S)))

    proof

      assume that

       A1: (P,Q,R,S) are_collinear and

       A2: (P,Q,R,S) are_mutually_distinct ;

      

       A3: P <> R & P <> S & R <> Q & S <> Q & S <> R & P <> Q by A2, ZFMISC_1:def 6;

      (P,R,Q,S) are_collinear by A1;

      then ( cross-ratio (S,Q,R,P)) = ( cross-ratio (P,R,Q,S)) by A3, Th34bis;

      hence thesis by A1, A2, Th35;

    end;

    definition

      let V be RealLinearSpace;

      let x be Tuple of 4, the carrier of V;

      :: ANPROJ10:def30

      func cross-ratio-tuple (x) -> Real means

      : Def03: ex P,Q,R,S be Element of V st P = (x . 1) & Q = (x . 2) & R = (x . 3) & S = (x . 4) & it = ( cross-ratio (P,Q,R,S));

      existence

      proof

        ( dom x) = ( Seg 4) by FINSEQ_2: 124;

        then 1 in ( dom x) & 2 in ( dom x) & 3 in ( dom x) & 4 in ( dom x);

        then

        reconsider P = (x . 1), Q = (x . 2), R = (x . 3), S = (x . 4) as Element of V by FINSEQ_2: 11;

        ( cross-ratio (P,Q,R,S)) is Real;

        hence thesis;

      end;

      uniqueness ;

    end

    theorem :: ANPROJ10:67

    

     Th36: x = <*P, Q, R, S*> implies ( cross-ratio (P,Q,R,S)) = ( cross-ratio-tuple x)

    proof

      assume x = <*P, Q, R, S*>;

      then (x . 1) = P & (x . 2) = Q & (x . 3) = R & (x . 4) = S;

      hence thesis by Def03;

    end;

    theorem :: ANPROJ10:68

    

     Th37: x = <*P, Q, R, S*> & (P,Q,R,S) are_collinear & P <> S & Q <> R & Q <> S implies ( cross-ratio-tuple x) = ( cross-ratio-tuple ( pi_3412 x))

    proof

      assume that

       A1: x = <*P, Q, R, S*> and

       A2: (P,Q,R,S) are_collinear and

       A3: P <> S and

       A4: Q <> R and

       A5: Q <> S;

      consider P9,Q9,R9,S9 be Element of V such that

       A7: P9 = (x . 1) & Q9 = (x . 2) & R9 = (x . 3) & S9 = (x . 4) & ( cross-ratio-tuple x) = ( cross-ratio (P9,Q9,R9,S9)) by Def03;

      ex P99,Q99,R99,S99 be Element of V st P99 = (( pi_3412 x) . 1) & Q99 = (( pi_3412 x) . 2) & R99 = (( pi_3412 x) . 3) & S99 = (( pi_3412 x) . 4) & ( cross-ratio-tuple ( pi_3412 x)) = ( cross-ratio (P99,Q99,R99,S99)) by Def03;

      hence thesis by A1, A7, A2, A3, A4, A5, Th33;

    end;

    theorem :: ANPROJ10:69

    

     Th38: x = <*P, Q, R, S*> & (P,Q,R,S) are_collinear & P <> R & P <> S & Q <> R & Q <> S implies ( cross-ratio-tuple x) = ( cross-ratio-tuple ( pi_2143 x)) & ( cross-ratio-tuple x) = ( cross-ratio-tuple ( pi_4321 x))

    proof

      assume that

       A1: x = <*P, Q, R, S*> and

       A2: (P,Q,R,S) are_collinear and

       A3: P <> R and

       A4: P <> S and

       A5: Q <> R and

       A6: Q <> S;

      

       A8: ex P9,Q9,R9,S9 be Element of V st P9 = (x . 1) & Q9 = (x . 2) & R9 = (x . 3) & S9 = (x . 4) & ( cross-ratio-tuple x) = ( cross-ratio (P9,Q9,R9,S9)) by Def03;

      

       H1: ex P99,Q99,R99,S99 be Element of V st P99 = (( pi_2143 x) . 1) & Q99 = (( pi_2143 x) . 2) & R99 = (( pi_2143 x) . 3) & S99 = (( pi_2143 x) . 4) & ( cross-ratio-tuple ( pi_2143 x)) = ( cross-ratio (P99,Q99,R99,S99)) by Def03;

      ex P99,Q99,R99,S99 be Element of V st P99 = (( pi_4321 x) . 1) & Q99 = (( pi_4321 x) . 2) & R99 = (( pi_4321 x) . 3) & S99 = (( pi_4321 x) . 4) & ( cross-ratio-tuple ( pi_4321 x)) = ( cross-ratio (P99,Q99,R99,S99)) by Def03;

      hence thesis by H1, A6, A1, A8, A2, A3, A4, A5, Th34, Th34bis;

    end;

    theorem :: ANPROJ10:70

    

     Th39: ( cross-ratio-tuple ( pi_1243 x)) = (1 / ( cross-ratio-tuple x))

    proof

      consider P9,Q9,R9,S9 be Element of V such that

       A1: P9 = (x . 1) & Q9 = (x . 2) & R9 = (x . 3) & S9 = (x . 4) & ( cross-ratio-tuple x) = ( cross-ratio (P9,Q9,R9,S9)) by Def03;

      ex P99,Q99,R99,S99 be Element of V st P99 = (( pi_1243 x) . 1) & Q99 = (( pi_1243 x) . 2) & R99 = (( pi_1243 x) . 3) & S99 = (( pi_1243 x) . 4) & ( cross-ratio-tuple ( pi_1243 x)) = ( cross-ratio (P99,Q99,R99,S99)) by Def03;

      hence thesis by A1, XCMPLX_1: 57;

    end;

    theorem :: ANPROJ10:71

    x = <*P, Q, R, S*> & (P,Q,R,S) are_mutually_distinct & (P,Q,R,S) are_collinear implies (ex r be non unit non zero Real st r = ( cross-ratio-tuple x) & ( cross-ratio-tuple ( pi_1243 x)) = ( op1 r))

    proof

      assume that

       A1: x = <*P, Q, R, S*> and

       A2: (P,Q,R,S) are_mutually_distinct and

       A3: (P,Q,R,S) are_collinear ;

      

       A4: P <> R & P <> S & R <> Q & S <> Q & S <> R & P <> Q by A2, ZFMISC_1:def 6;

      consider P9,Q9,R9,S9 be Element of V such that

       A5: P9 = (x . 1) & Q9 = (x . 2) & R9 = (x . 3) & S9 = (x . 4) & ( cross-ratio-tuple x) = ( cross-ratio (P9,Q9,R9,S9)) by Def03;

      reconsider r = ( cross-ratio-tuple x) as non unit non zero Real by Def01, A1, A3, A5, A4, Th32, Th31;

      take r;

      thus thesis by Th39;

    end;

    theorem :: ANPROJ10:72

    

     Th40: x = <*P, Q, R, S*> & (P,Q,R,S) are_collinear & P <> R & P <> S & Q <> R & Q <> S implies ( cross-ratio-tuple ( pi_1243 x)) = (1 / ( cross-ratio-tuple x)) & ( cross-ratio-tuple ( pi_2134 x)) = (1 / ( cross-ratio-tuple x)) & ( cross-ratio-tuple ( pi_3421 x)) = (1 / ( cross-ratio-tuple x)) & ( cross-ratio-tuple ( pi_4312 x)) = (1 / ( cross-ratio-tuple x))

    proof

      assume that

       A1: x = <*P, Q, R, S*> and

       A2: (P,Q,R,S) are_collinear and

       A3: P <> R and

       A4: P <> S and

       A5: Q <> R and

       A6: Q <> S;

      

       A7: ( pi_1243 x) = <*P, Q, S, R*> & (P,Q,S,R) are_collinear by A2, A1;

      consider P9,Q9,R9,S9 be Element of V such that

       A8: P9 = (x . 1) & Q9 = (x . 2) & R9 = (x . 3) & S9 = (x . 4) & ( cross-ratio-tuple x) = ( cross-ratio (P9,Q9,R9,S9)) by Def03;

      consider P99,Q99,R99,S99 be Element of V such that

       A9: P99 = (( pi_1243 x) . 1) & Q99 = (( pi_1243 x) . 2) & R99 = (( pi_1243 x) . 3) & S99 = (( pi_1243 x) . 4) & ( cross-ratio-tuple ( pi_1243 x)) = ( cross-ratio (P99,Q99,R99,S99)) by Def03;

      now

        

        thus ( cross-ratio-tuple ( pi_2134 x)) = ( cross-ratio-tuple ( pi_2143 ( pi_1243 x)))

        .= ( cross-ratio-tuple ( pi_1243 x)) by A7, A3, A4, A5, A6, Th38;

        

        thus ( cross-ratio-tuple ( pi_3421 x)) = ( cross-ratio-tuple ( pi_4321 ( pi_1243 x)))

        .= ( cross-ratio-tuple ( pi_1243 x)) by A7, A3, A4, A5, A6, Th38;

        

        thus ( cross-ratio-tuple ( pi_4312 x)) = ( cross-ratio-tuple ( pi_3412 ( pi_1243 x)))

        .= ( cross-ratio-tuple ( pi_1243 x)) by A7, A3, A5, A6, Th37;

      end;

      hence thesis by A8, A9, XCMPLX_1: 57;

    end;

    theorem :: ANPROJ10:73

    

     Th41: x = <*P, Q, R, S*> & (P,Q,R,S) are_mutually_distinct & (P,Q,R,S) are_collinear implies ( cross-ratio-tuple ( pi_1324 x)) = (1 - ( cross-ratio-tuple x)) & ( cross-ratio-tuple ( pi_2413 x)) = (1 - ( cross-ratio-tuple x)) & ( cross-ratio-tuple ( pi_3142 x)) = (1 - ( cross-ratio-tuple x)) & ( cross-ratio-tuple ( pi_4231 x)) = (1 - ( cross-ratio-tuple x))

    proof

      assume that

       A1: x = <*P, Q, R, S*> and

       A2: (P,Q,R,S) are_mutually_distinct and

       A3: (P,Q,R,S) are_collinear ;

      

       A4: P <> R & P <> S & R <> Q & S <> Q & S <> R & P <> Q by A2, ZFMISC_1:def 6;

      

       A6: ( pi_1324 x) = <*P, R, Q, S*> & (P,R,Q,S) are_collinear by A3, A1;

      now

        (x . 1) = P & (x . 2) = Q & (x . 3) = R & (x . 4) = S & (( pi_1324 x) . 1) = P & (( pi_1324 x) . 2) = R & (( pi_1324 x) . 3) = Q & (( pi_1324 x) . 4) = S by A1;

        hence ( cross-ratio-tuple ( pi_1324 x)) = ( cross-ratio (P,R,Q,S)) & ( cross-ratio-tuple x) = ( cross-ratio (P,Q,R,S)) by Def03;

        

        thus ( cross-ratio-tuple ( pi_2413 x)) = ( cross-ratio-tuple ( pi_3412 ( pi_1324 x)))

        .= ( cross-ratio-tuple ( pi_1324 x)) by A6, A4, Th37;

        

        thus ( cross-ratio-tuple ( pi_3142 x)) = ( cross-ratio-tuple ( pi_2143 ( pi_1324 x)))

        .= ( cross-ratio-tuple ( pi_1324 x)) by A4, Th38, A6;

        

        thus ( cross-ratio-tuple ( pi_4231 x)) = ( cross-ratio-tuple ( pi_4321 ( pi_1324 x)))

        .= ( cross-ratio-tuple ( pi_1324 x)) by A4, Th38, A6;

      end;

      hence thesis by A2, A3, Th35;

    end;

    theorem :: ANPROJ10:74

    x = <*P, Q, R, S*> & (P,Q,R,S) are_mutually_distinct & (P,Q,R,S) are_collinear implies ( cross-ratio-tuple ( pi_3124 x)) = (1 / (1 - ( cross-ratio-tuple x))) & ( cross-ratio-tuple ( pi_2431 x)) = (1 / (1 - ( cross-ratio-tuple x))) & ( cross-ratio-tuple ( pi_1342 x)) = (1 / (1 - ( cross-ratio-tuple x))) & ( cross-ratio-tuple ( pi_4213 x)) = (1 / (1 - ( cross-ratio-tuple x)))

    proof

      assume that

       A1: x = <*P, Q, R, S*> and

       A2: (P,Q,R,S) are_mutually_distinct and

       A3: (P,Q,R,S) are_collinear ;

      

       A4: P <> R & P <> S & R <> Q & S <> Q & S <> R & P <> Q by A2, ZFMISC_1:def 6;

      

       A7: ( cross-ratio-tuple ( pi_1243 ( pi_3142 x))) = (1 / ( cross-ratio-tuple ( pi_3142 x))) by Th39;

      hence ( cross-ratio-tuple ( pi_3124 x)) = (1 / (1 - ( cross-ratio-tuple x))) by A2, A3, A1, Th41;

      

       A8: ( pi_3124 x) = <*R, P, Q, S*> & (R,P,Q,S) are_collinear by A3, A1;

      now

        

        thus ( cross-ratio-tuple ( pi_3412 ( pi_3124 x))) = ( cross-ratio-tuple ( pi_3124 x)) by A8, Th37, A4

        .= (1 / (1 - ( cross-ratio-tuple x))) by A3, A7, A1, A2, Th41;

        

        thus ( cross-ratio-tuple ( pi_2143 ( pi_3124 x))) = ( cross-ratio-tuple ( pi_3124 x)) by A8, A4, Th38

        .= (1 / (1 - ( cross-ratio-tuple x))) by A3, A7, A1, A2, Th41;

        

        thus ( cross-ratio-tuple ( pi_4321 ( pi_3124 x))) = ( cross-ratio-tuple ( pi_3124 x)) by A4, A8, Th38

        .= (1 / (1 - ( cross-ratio-tuple x))) by A3, A7, A1, A2, Th41;

      end;

      hence thesis;

    end;

    theorem :: ANPROJ10:75

    

     Th42: x = <*P, Q, R, S*> & (P,Q,R,S) are_mutually_distinct & (P,Q,R,S) are_collinear implies ( cross-ratio-tuple ( pi_1423 x)) = ((( cross-ratio-tuple x) - 1) / ( cross-ratio-tuple x)) & ( cross-ratio-tuple ( pi_2314 x)) = ((( cross-ratio-tuple x) - 1) / ( cross-ratio-tuple x)) & ( cross-ratio-tuple ( pi_4132 x)) = ((( cross-ratio-tuple x) - 1) / ( cross-ratio-tuple x)) & ( cross-ratio-tuple ( pi_3241 x)) = ((( cross-ratio-tuple x) - 1) / ( cross-ratio-tuple x))

    proof

      assume that

       A1: x = <*P, Q, R, S*> and

       A2: (P,Q,R,S) are_mutually_distinct and

       A3: (P,Q,R,S) are_collinear ;

      

       A4: P <> R & P <> S & R <> Q & S <> Q & S <> R & P <> Q by A2, ZFMISC_1:def 6;

      ( cross-ratio (P,Q,R,S)) <> 0 by A3, A4, Th31;

      then

      reconsider cr = ( cross-ratio-tuple x) as non zero Complex by A1, Th36;

      ( pi_1243 x) = <*P, Q, S, R*> & (P,Q,S,R) are_collinear & (P,Q,S,R) are_mutually_distinct by A4, A1, A3, ZFMISC_1:def 6;

      

      then

       A5: ( cross-ratio-tuple ( pi_1324 ( pi_1243 x))) = (1 - ( cross-ratio-tuple ( pi_1243 x))) by Th41

      .= (1 - (1 / cr)) by A1, A3, A4, Th40

      .= ((cr / cr) - (1 / cr)) by XCMPLX_1: 60

      .= ((cr - 1) / cr);

      hence ( cross-ratio-tuple ( pi_1423 x)) = ((( cross-ratio-tuple x) - 1) / ( cross-ratio-tuple x));

      ( pi_1423 x) = <*P, S, Q, R*> & (P,S,Q,R) are_collinear by A1, A3;

      then ( cross-ratio-tuple ( pi_3412 ( pi_1423 x))) = ( cross-ratio-tuple ( pi_1423 x)) & ( cross-ratio-tuple ( pi_2143 ( pi_1423 x))) = ( cross-ratio-tuple ( pi_1423 x)) & ( cross-ratio-tuple ( pi_4321 ( pi_1423 x))) = ( cross-ratio-tuple ( pi_1423 x)) by A4, Th37, Th38;

      hence thesis by A5;

    end;

    theorem :: ANPROJ10:76

    x = <*P, Q, R, S*> & (P,Q,R,S) are_mutually_distinct & (P,Q,R,S) are_collinear implies ( cross-ratio-tuple ( pi_1432 x)) = (( cross-ratio-tuple x) / (( cross-ratio-tuple x) - 1)) & ( cross-ratio-tuple ( pi_2341 x)) = (( cross-ratio-tuple x) / (( cross-ratio-tuple x) - 1)) & ( cross-ratio-tuple ( pi_3214 x)) = (( cross-ratio-tuple x) / (( cross-ratio-tuple x) - 1)) & ( cross-ratio-tuple ( pi_4123 x)) = (( cross-ratio-tuple x) / (( cross-ratio-tuple x) - 1))

    proof

      assume that

       A1: x = <*P, Q, R, S*> and

       A2: (P,Q,R,S) are_mutually_distinct and

       A3: (P,Q,R,S) are_collinear ;

      

       A4: P <> R & P <> S & R <> Q & S <> Q & S <> R & P <> Q by A2, ZFMISC_1:def 6;

      

       A5: (P,S,R,Q) are_collinear & ( pi_1432 x) = <*P, S, R, Q*> by A1, A3;

      

       A6: ( cross-ratio-tuple ( pi_1432 x)) = ( cross-ratio-tuple ( pi_1243 ( pi_1423 x)))

      .= (1 / ( cross-ratio-tuple ( pi_1423 x))) by Th39

      .= (1 / ((( cross-ratio-tuple x) - 1) / ( cross-ratio-tuple x))) by A1, A3, A2, Th42;

      hence ( cross-ratio-tuple ( pi_1432 x)) = (( cross-ratio-tuple x) / (( cross-ratio-tuple x) - 1)) by XCMPLX_1: 57;

      now

        

        thus ( cross-ratio-tuple ( pi_2341 x)) = ( cross-ratio-tuple ( pi_4321 ( pi_1432 x)))

        .= ( cross-ratio-tuple ( pi_1432 x)) by A5, A4, Th38;

        

        thus ( cross-ratio-tuple ( pi_3214 x)) = ( cross-ratio-tuple ( pi_3412 ( pi_1432 x)))

        .= ( cross-ratio-tuple ( pi_1432 x)) by A4, A5, Th37;

        

        thus ( cross-ratio-tuple ( pi_4123 x)) = ( cross-ratio-tuple ( pi_2143 ( pi_1432 x)))

        .= ( cross-ratio-tuple ( pi_1432 x)) by A4, A5, Th38;

      end;

      hence thesis by A6, XCMPLX_1: 57;

    end;

    begin

    

     Lm03: for a,b,c,d be Complex holds (((a - c) / (b - c)) / ((a - d) / (b - d))) = (((c - a) / (c - b)) * ((d - b) / (d - a)))

    proof

      let a,b,c,d be Complex;

      (((a - c) / (b - c)) / ((a - d) / (b - d))) = (((( - 1) * (c - a)) / (( - 1) * (c - b))) / ((( - 1) * (d - a)) / (( - 1) * (d - b))))

      .= (((c - a) / (c - b)) / ((( - 1) * (d - a)) / (( - 1) * (d - b)))) by XCMPLX_1: 91

      .= (((c - a) / (c - b)) / ((d - a) / (d - b))) by XCMPLX_1: 91

      .= (((c - a) / (c - b)) * ((d - b) / (d - a))) by XCMPLX_1: 79;

      hence thesis;

    end;

    theorem :: ANPROJ10:77

    for x1,x2,x3,x4 be Element of ( TOP-REAL 1) st x2 <> x3 & x3 <> x1 & x2 <> x4 & x1 <> x4 holds ex a,b,c,d be Real st x1 = <*a*> & x2 = <*b*> & x3 = <*c*> & x4 = <*d*> & ( cross-ratio-tuple <*x1, x2, x3, x4*>) = (((c - a) / (c - b)) * ((d - b) / (d - a)))

    proof

      let x1,x2,x3,x4 be Element of ( TOP-REAL 1);

      assume that

       A1: x2 <> x3 and

       A2: x3 <> x1 and

       A3: x2 <> x4 and

       A4: x1 <> x4;

      reconsider x = <*x1, x2, x3, x4*> as Tuple of 4, the carrier of ( TOP-REAL 1);

      consider P,Q,R,S be Element of ( TOP-REAL 1) such that

       A5: P = (x . 1) & Q = (x . 2) & R = (x . 3) & S = (x . 4) & ( cross-ratio-tuple x) = ( cross-ratio (P,Q,R,S)) by Def03;

      consider a1,b1,c1 be Real such that

       A7: x3 = <*a1*> & x1 = <*b1*> & x2 = <*c1*> & ( affine-ratio (x3,x1,x2)) = ((b1 - a1) / (c1 - a1)) by A1, A2, Th26;

      consider a2,b2,c2 be Real such that

       A8: x4 = <*a2*> & x1 = <*b2*> & x2 = <*c2*> & ( affine-ratio (x4,x1,x2)) = ((b2 - a2) / (c2 - a2)) by A3, A4, Th26;

      take b1, c1, a1, a2;

      b1 = b2 & c1 = c2 by A7, A8, FINSEQ_1: 76;

      hence thesis by A7, A8, Lm03, A5;

    end;