anproj_2.miz

    begin

    reserve V for RealLinearSpace,

o,p,q,r,s,u,v,w,y,y1,u1,v1,w1,u2,v2,w2 for Element of V,

a,b,c,d,a1,b1,c1,d1,a2,b2,c2,d2,a3,b3,c3,d3 for Real,

z for set;

    theorem :: ANPROJ_2:1



     Th1: (for a, b, c st (((a * u) + (b * v)) + (c * w)) = ( 0. V) holds a = 0 & b = 0 & c = 0 ) implies not u is zero & not v is zero & not w is zero & not (u,v,w) are_LinDep & not are_Prop (u,v)

    proof

      assume

       A1: for a, b, c st (((a * u) + (b * v)) + (c * w)) = ( 0. V) holds a = 0 & b = 0 & c = 0 ;

       A2:

      now

        assume not not v is zero;

        then

         A3: v = ( 0. V);

        ( 0. V) = (( 0. V) + ( 0. V)) by RLVECT_1: 4

        .= ((( 0. V) + ( 0. V)) + ( 0. V)) by RLVECT_1: 4

        .= ((( 0. V) + (1 * v)) + ( 0. V)) by A3, RLVECT_1:def 8

        .= ((( 0 * u) + (1 * v)) + ( 0. V)) by RLVECT_1: 10

        .= ((( 0 * u) + (1 * v)) + ( 0 * w)) by RLVECT_1: 10;

        hence contradiction by A1;

      end;

       A4:

      now

        assume not not w is zero;

        then

         A5: w = ( 0. V);

        ( 0. V) = (( 0. V) + ( 0. V)) by RLVECT_1: 4

        .= ((( 0. V) + ( 0. V)) + ( 0. V)) by RLVECT_1: 4

        .= ((( 0. V) + ( 0. V)) + (1 * w)) by A5, RLVECT_1:def 8

        .= ((( 0 * u) + ( 0. V)) + (1 * w)) by RLVECT_1: 10

        .= ((( 0 * u) + ( 0 * v)) + (1 * w)) by RLVECT_1: 10;

        hence contradiction by A1;

      end;

      now

        assume not not u is zero;

        then

         A6: u = ( 0. V);

        ( 0. V) = (( 0. V) + ( 0. V)) by RLVECT_1: 4

        .= ((( 0. V) + ( 0. V)) + ( 0. V)) by RLVECT_1: 4

        .= (((1 * u) + ( 0. V)) + ( 0. V)) by A6, RLVECT_1:def 8

        .= (((1 * u) + ( 0 * v)) + ( 0. V)) by RLVECT_1: 10

        .= (((1 * u) + ( 0 * v)) + ( 0 * w)) by RLVECT_1: 10;

        hence contradiction by A1;

      end;

      hence not u is zero & not v is zero & not w is zero by A2, A4;

      thus not (u,v,w) are_LinDep by A1;

      hence thesis by ANPROJ_1: 12;

    end;



     Lm1: (for a, b st ((a * u) + (b * v)) = ( 0. V) holds a = 0 & b = 0 ) implies not u is zero & not v is zero & not are_Prop (u,v)

    proof

      assume

       A1: for a, b st ((a * u) + (b * v)) = ( 0. V) holds a = 0 & b = 0 ;

       A2:

      now

        assume not not v is zero;

        then

         A3: v = ( 0. V);

        ( 0. V) = (( 0. V) + ( 0. V)) by RLVECT_1: 4

        .= (( 0. V) + (1 * v)) by A3, RLVECT_1:def 8

        .= (( 0 * u) + (1 * v)) by RLVECT_1: 10;

        hence contradiction by A1;

      end;

      now

        assume not not u is zero;

        then

         A4: u = ( 0. V);

        ( 0. V) = (( 0. V) + ( 0. V)) by RLVECT_1: 4

        .= ((1 * u) + ( 0. V)) by A4, RLVECT_1:def 8

        .= ((1 * u) + ( 0 * v)) by RLVECT_1: 10;

        hence contradiction by A1;

      end;

      hence not u is zero & not v is zero by A2;

      given a, b such that

       A5: (a * u) = (b * v) and

       A6: a <> 0 and b <> 0 ;

      ( 0. V) = ((a * u) - (b * v)) by A5, RLVECT_1: 15

      .= ((a * u) + (b * ( - v))) by RLVECT_1: 25

      .= ((a * u) + (( - b) * v)) by RLVECT_1: 24;

      hence contradiction by A1, A6;

    end;

    theorem :: ANPROJ_2:2



     Th2: for u, v, u1, v1 holds ((for a, b, a1, b1 st ((((a * u) + (b * v)) + (a1 * u1)) + (b1 * v1)) = ( 0. V) holds a = 0 & b = 0 & a1 = 0 & b1 = 0 ) implies not u is zero & not v is zero & not are_Prop (u,v) & not u1 is zero & not v1 is zero & not are_Prop (u1,v1) & not (u,v,u1) are_LinDep & not (u1,v1,u) are_LinDep )

    proof

      let u, v, u1, v1;

      assume

       A1: for a, b, a1, b1 st ((((a * u) + (b * v)) + (a1 * u1)) + (b1 * v1)) = ( 0. V) holds a = 0 & b = 0 & a1 = 0 & b1 = 0 ;

       A2:

      now

        let d1, d2, d3;

        assume (((d1 * u) + (d2 * v)) + (d3 * u1)) = ( 0. V);



        then ( 0. V) = ((((d1 * u) + (d2 * v)) + (d3 * u1)) + ( 0. V)) by RLVECT_1: 4

        .= ((((d1 * u) + (d2 * v)) + (d3 * u1)) + ( 0 * v1)) by RLVECT_1: 10;

        hence d1 = 0 & d2 = 0 & d3 = 0 by A1;

      end;

      now

        let d1, d2, d3;

        assume (((d1 * u1) + (d2 * v1)) + (d3 * u)) = ( 0. V);



        then ( 0. V) = (((d3 * u) + (d1 * u1)) + (d2 * v1)) by RLVECT_1:def 3

        .= ((((d3 * u) + ( 0. V)) + (d1 * u1)) + (d2 * v1)) by RLVECT_1: 4

        .= ((((d3 * u) + ( 0 * v)) + (d1 * u1)) + (d2 * v1)) by RLVECT_1: 10;

        hence d1 = 0 & d2 = 0 & d3 = 0 by A1;

      end;

      hence thesis by A2, Th1;

    end;



     Lm2: (a * (((b * v) + (c * w)) + (d * u))) = ((((a * b) * v) + ((a * c) * w)) + ((a * d) * u))

    proof



      thus ((((a * b) * v) + ((a * c) * w)) + ((a * d) * u)) = (((a * (b * v)) + ((a * c) * w)) + ((a * d) * u)) by RLVECT_1:def 7

      .= (((a * (b * v)) + (a * (c * w))) + ((a * d) * u)) by RLVECT_1:def 7

      .= ((a * ((b * v) + (c * w))) + ((a * d) * u)) by RLVECT_1:def 5

      .= ((a * ((b * v) + (c * w))) + (a * (d * u))) by RLVECT_1:def 7

      .= (a * (((b * v) + (c * w)) + (d * u))) by RLVECT_1:def 5;

    end;



     Lm3: (((u + v) + w) + ((u1 + v1) + w1)) = (((u + u1) + (v + v1)) + (w + w1))

    proof



      thus (((u + u1) + (v + v1)) + (w + w1)) = ((u1 + (u + (v + v1))) + (w + w1)) by RLVECT_1:def 3

      .= ((u1 + ((u + v) + v1)) + (w + w1)) by RLVECT_1:def 3

      .= (((u1 + v1) + (u + v)) + (w + w1)) by RLVECT_1:def 3

      .= ((u1 + v1) + ((u + v) + (w + w1))) by RLVECT_1:def 3

      .= ((u1 + v1) + (((u + v) + w) + w1)) by RLVECT_1:def 3

      .= (((u + v) + w) + ((u1 + v1) + w1)) by RLVECT_1:def 3;

    end;

    theorem :: ANPROJ_2:3



     Th3: (for w holds ex a, b, c st w = (((a * p) + (b * q)) + (c * r))) & (for a, b, c st (((a * p) + (b * q)) + (c * r)) = ( 0. V) holds a = 0 & b = 0 & c = 0 ) implies for u, u1 holds ex y st (p,q,y) are_LinDep & (u,u1,y) are_LinDep & not y is zero

    proof

      assume that

       A1: for w holds ex a, b, c st w = (((a * p) + (b * q)) + (c * r)) and

       A2: for a, b, c st (((a * p) + (b * q)) + (c * r)) = ( 0. V) holds a = 0 & b = 0 & c = 0 ;

      let u, u1;

      consider a, b, c such that

       A3: u = (((a * p) + (b * q)) + (c * r)) by A1;

      consider a1, b1, c1 such that

       A4: u1 = (((a1 * p) + (b1 * q)) + (c1 * r)) by A1;



       A5: ((a3 * u) + (b3 * u1)) = (((((a3 * a) + (b3 * a1)) * p) + (((a3 * b) + (b3 * b1)) * q)) + (((a3 * c) + (b3 * c1)) * r))

      proof

        (a3 * u) = ((((a3 * a) * p) + ((a3 * b) * q)) + ((a3 * c) * r)) by A3, Lm2;



        hence ((a3 * u) + (b3 * u1)) = (((((a3 * a) * p) + ((a3 * b) * q)) + ((a3 * c) * r)) + ((((b3 * a1) * p) + ((b3 * b1) * q)) + ((b3 * c1) * r))) by A4, Lm2

        .= (((((a3 * a) * p) + ((b3 * a1) * p)) + (((a3 * b) * q) + ((b3 * b1) * q))) + (((a3 * c) * r) + ((b3 * c1) * r))) by Lm3

        .= (((((a3 * a) + (b3 * a1)) * p) + (((a3 * b) * q) + ((b3 * b1) * q))) + (((a3 * c) * r) + ((b3 * c1) * r))) by RLVECT_1:def 6

        .= (((((a3 * a) + (b3 * a1)) * p) + (((a3 * b) + (b3 * b1)) * q)) + (((a3 * c) * r) + ((b3 * c1) * r))) by RLVECT_1:def 6

        .= (((((a3 * a) + (b3 * a1)) * p) + (((a3 * b) + (b3 * b1)) * q)) + (((a3 * c) + (b3 * c1)) * r)) by RLVECT_1:def 6;

      end;



       A6: not q is zero by A2, Th1;

       A7:

      now

         A8:

        now

          assume not not u1 is zero;

          then u1 = ( 0. V);

          then (p,q,q) are_LinDep & (u,u1,q) are_LinDep by ANPROJ_1: 10, ANPROJ_1: 11;

          hence thesis by A6;

        end;

         A9:

        now

          assume not not u is zero;

          then u = ( 0. V);

          then (p,q,q) are_LinDep & (u,u1,q) are_LinDep by ANPROJ_1: 10, ANPROJ_1: 11;

          hence thesis by A6;

        end;

         A10:

        now

          assume are_Prop (u,u1);

          then (p,q,q) are_LinDep & (u,u1,q) are_LinDep by ANPROJ_1: 11;

          hence thesis by A6;

        end;

        assume are_Prop (u,u1) or not not u is zero or not not u1 is zero;

        hence thesis by A10, A9, A8;

      end;



       A11: not p is zero & not are_Prop (p,q) by A2, Th1;

       A12:

      now

        assume that

         A13: not are_Prop (u,u1) and

         A14: not u is zero and

         A15: not u1 is zero and

         A16: c <> 0 ;

         A17:

        now

          set a3 = 1, b3 = ( - (c * (c1 " )));

          set y = ((a3 * u) + (b3 * u1));

          assume

           A18: c1 <> 0 ;

          then (c1 " ) <> 0 by XCMPLX_1: 202;

          then

           A19: (c * (c1 " )) <> 0 by A16, XCMPLX_1: 6;



           A20: not y is zero

          proof

            assume not not y is zero;



            then ( 0. V) = ((1 * u) + (( - (c * (c1 " ))) * u1))

            .= ((1 * u) + ((c * (c1 " )) * ( - u1))) by RLVECT_1: 24

            .= ((1 * u) + ( - ((c * (c1 " )) * u1))) by RLVECT_1: 25;

            then ( - (1 * u)) = ( - ((c * (c1 " )) * u1)) by RLVECT_1:def 10;

            then (1 * u) = ((c * (c1 " )) * u1) by RLVECT_1: 18;

            hence contradiction by A13, A19;

          end;

          ((a3 * c) + (b3 * c1)) = (c + (( - c) * ((c1 " ) * c1)))

          .= (c + (( - c) * 1)) by A18, XCMPLX_0:def 7

          .= 0 ;



          then y = (((((a3 * a) + (b3 * a1)) * p) + (((a3 * b) + (b3 * b1)) * q)) + ( 0 * r)) by A5

          .= (((((a3 * a) + (b3 * a1)) * p) + (((a3 * b) + (b3 * b1)) * q)) + ( 0. V)) by RLVECT_1: 10

          .= ((((a3 * a) + (b3 * a1)) * p) + (((a3 * b) + (b3 * b1)) * q)) by RLVECT_1: 4;

          then

           A21: (p,q,y) are_LinDep by A6, A11, ANPROJ_1: 6;

          (u,u1,y) are_LinDep by A13, A14, A15, ANPROJ_1: 6;

          hence thesis by A20, A21;

        end;

        now

          set a3 = 0 , b3 = 1;

          set y = ((a3 * u) + (b3 * u1));



           A22: y = (( 0 * u) + u1) by RLVECT_1:def 8

          .= (( 0. V) + u1) by RLVECT_1: 10

          .= u1 by RLVECT_1: 4;

          assume c1 = 0 ;

          then ((a3 * c) + (b3 * c1)) = 0 ;



          then y = (((((a3 * a) + (b3 * a1)) * p) + (((a3 * b) + (b3 * b1)) * q)) + ( 0 * r)) by A5

          .= (((((a3 * a) + (b3 * a1)) * p) + (((a3 * b) + (b3 * b1)) * q)) + ( 0. V)) by RLVECT_1: 10

          .= ((((a3 * a) + (b3 * a1)) * p) + (((a3 * b) + (b3 * b1)) * q)) by RLVECT_1: 4;

          then

           A23: (p,q,y) are_LinDep by A6, A11, ANPROJ_1: 6;

          (u,u1,y) are_LinDep by A13, A14, A15, ANPROJ_1: 6;

          hence thesis by A15, A22, A23;

        end;

        hence thesis by A17;

      end;

      now

        assume that

         A24: not are_Prop (u,u1) and

         A25: not u is zero and

         A26: not u1 is zero and

         A27: c = 0 ;

        now

          set a3 = 1, b3 = 0 ;

          set y = ((a3 * u) + (b3 * u1));



           A28: y = (u + ( 0 * u1)) by RLVECT_1:def 8

          .= (u + ( 0. V)) by RLVECT_1: 10

          .= u by RLVECT_1: 4;

          ((a3 * c) + (b3 * c1)) = 0 by A27;



          then y = (((((a3 * a) + (b3 * a1)) * p) + (((a3 * b) + (b3 * b1)) * q)) + ( 0 * r)) by A5

          .= (((((a3 * a) + (b3 * a1)) * p) + (((a3 * b) + (b3 * b1)) * q)) + ( 0. V)) by RLVECT_1: 10

          .= ((((a3 * a) + (b3 * a1)) * p) + (((a3 * b) + (b3 * b1)) * q)) by RLVECT_1: 4;

          then

           A29: (p,q,y) are_LinDep by A6, A11, ANPROJ_1: 6;

          (u,u1,y) are_LinDep by A24, A25, A26, ANPROJ_1: 6;

          hence thesis by A25, A28, A29;

        end;

        hence thesis;

      end;

      hence thesis by A7, A12;

    end;



     Lm4: (a * ((((b * v) + (c * w)) + (d * u)) + (d1 * y))) = (((((a * b) * v) + ((a * c) * w)) + ((a * d) * u)) + ((a * d1) * y))

    proof



      thus (((((a * b) * v) + ((a * c) * w)) + ((a * d) * u)) + ((a * d1) * y)) = ((((a * (b * v)) + ((a * c) * w)) + ((a * d) * u)) + ((a * d1) * y)) by RLVECT_1:def 7

      .= ((((a * (b * v)) + (a * (c * w))) + ((a * d) * u)) + ((a * d1) * y)) by RLVECT_1:def 7

      .= (((a * ((b * v) + (c * w))) + ((a * d) * u)) + ((a * d1) * y)) by RLVECT_1:def 5

      .= (((a * ((b * v) + (c * w))) + (a * (d * u))) + ((a * d1) * y)) by RLVECT_1:def 7

      .= (((a * ((b * v) + (c * w))) + (a * (d * u))) + (a * (d1 * y))) by RLVECT_1:def 7

      .= ((a * (((b * v) + (c * w)) + (d * u))) + (a * (d1 * y))) by RLVECT_1:def 5

      .= (a * ((((b * v) + (c * w)) + (d * u)) + (d1 * y))) by RLVECT_1:def 5;

    end;



     Lm5: ((((u + v) + w) + y) + (((u1 + v1) + w1) + y1)) = ((((u + u1) + (v + v1)) + (w + w1)) + (y + y1))

    proof



      thus ((((u + u1) + (v + v1)) + (w + w1)) + (y + y1)) = (((u1 + (u + (v + v1))) + (w + w1)) + (y + y1)) by RLVECT_1:def 3

      .= (((u1 + ((u + v) + v1)) + (w + w1)) + (y + y1)) by RLVECT_1:def 3

      .= ((((u1 + v1) + (u + v)) + (w + w1)) + (y + y1)) by RLVECT_1:def 3

      .= (((u1 + v1) + ((u + v) + (w + w1))) + (y + y1)) by RLVECT_1:def 3

      .= (((u1 + v1) + (((u + v) + w) + w1)) + (y + y1)) by RLVECT_1:def 3

      .= ((((u1 + v1) + w1) + ((u + v) + w)) + (y + y1)) by RLVECT_1:def 3

      .= (((u + v) + w) + (((u1 + v1) + w1) + (y + y1))) by RLVECT_1:def 3

      .= (((u + v) + w) + (y + (y1 + ((u1 + v1) + w1)))) by RLVECT_1:def 3

      .= ((((u + v) + w) + y) + (((u1 + v1) + w1) + y1)) by RLVECT_1:def 3;

    end;



     Lm6: (a * (((b * v) + (c * w)) + (d * u))) = ((((a * b) * v) + ((a * c) * w)) + ((a * d) * u))

    proof



      thus ((((a * b) * v) + ((a * c) * w)) + ((a * d) * u)) = (((a * (b * v)) + ((a * c) * w)) + ((a * d) * u)) by RLVECT_1:def 7

      .= (((a * (b * v)) + (a * (c * w))) + ((a * d) * u)) by RLVECT_1:def 7

      .= ((a * ((b * v) + (c * w))) + ((a * d) * u)) by RLVECT_1:def 5

      .= ((a * ((b * v) + (c * w))) + (a * (d * u))) by RLVECT_1:def 7

      .= (a * (((b * v) + (c * w)) + (d * u))) by RLVECT_1:def 5;

    end;



     Lm7: y = ((a1 * p) + (b1 * w)) & w = (((a * p) + (b * q)) + (c * r)) implies y = ((((a1 + (b1 * a)) * p) + ((b1 * b) * q)) + ((b1 * c) * r))

    proof

      assume y = ((a1 * p) + (b1 * w)) & w = (((a * p) + (b * q)) + (c * r));



      hence y = ((a1 * p) + ((((b1 * a) * p) + ((b1 * b) * q)) + ((b1 * c) * r))) by Lm6

      .= ((a1 * p) + (((b1 * a) * p) + (((b1 * b) * q) + ((b1 * c) * r)))) by RLVECT_1:def 3

      .= (((a1 * p) + ((b1 * a) * p)) + (((b1 * b) * q) + ((b1 * c) * r))) by RLVECT_1:def 3

      .= (((a1 + (b1 * a)) * p) + (((b1 * b) * q) + ((b1 * c) * r))) by RLVECT_1:def 6

      .= ((((a1 + (b1 * a)) * p) + ((b1 * b) * q)) + ((b1 * c) * r)) by RLVECT_1:def 3;

    end;

    theorem :: ANPROJ_2:4



     Th4: (for w holds ex a, b, c, d st w = ((((a * p) + (b * q)) + (c * r)) + (d * s))) & (for a, b, c, d st ((((a * p) + (b * q)) + (c * r)) + (d * s)) = ( 0. V) holds a = 0 & b = 0 & c = 0 & d = 0 ) implies for u, v st not u is zero & not v is zero holds ex y, w st (u,v,w) are_LinDep & (q,r,y) are_LinDep & (p,w,y) are_LinDep & not y is zero & not w is zero

    proof

      assume that

       A1: for w holds ex a, b, c, d st w = ((((a * p) + (b * q)) + (c * r)) + (d * s)) and

       A2: for a, b, c, d st ((((a * p) + (b * q)) + (c * r)) + (d * s)) = ( 0. V) holds a = 0 & b = 0 & c = 0 & d = 0 ;



       A3: not p is zero by A2, Th2;

      let u, v such that

       A4: not u is zero and

       A5: not v is zero;

      consider a1, b1, c1, d1 such that

       A6: u = ((((a1 * p) + (b1 * q)) + (c1 * r)) + (d1 * s)) by A1;

       not (p,q,r) are_LinDep by A2, Th2;

      then

       A7: not are_Prop (q,r) by ANPROJ_1: 11;



       A8: not q is zero by A2, Th2;

      consider a2, b2, c2, d2 such that

       A9: v = ((((a2 * p) + (b2 * q)) + (c2 * r)) + (d2 * s)) by A1;



       A10: ((a3 * u) + (b3 * v)) = ((((((a3 * a1) + (b3 * a2)) * p) + (((a3 * b1) + (b3 * b2)) * q)) + (((a3 * c1) + (b3 * c2)) * r)) + (((a3 * d1) + (b3 * d2)) * s))

      proof

        (a3 * u) = (((((a3 * a1) * p) + ((a3 * b1) * q)) + ((a3 * c1) * r)) + ((a3 * d1) * s)) by A6, Lm4;



        hence ((a3 * u) + (b3 * v)) = ((((((a3 * a1) * p) + ((a3 * b1) * q)) + ((a3 * c1) * r)) + ((a3 * d1) * s)) + (((((b3 * a2) * p) + ((b3 * b2) * q)) + ((b3 * c2) * r)) + ((b3 * d2) * s))) by A9, Lm4

        .= ((((((a3 * a1) * p) + ((b3 * a2) * p)) + (((a3 * b1) * q) + ((b3 * b2) * q))) + (((a3 * c1) * r) + ((b3 * c2) * r))) + (((a3 * d1) * s) + ((b3 * d2) * s))) by Lm5

        .= ((((((a3 * a1) + (b3 * a2)) * p) + (((a3 * b1) * q) + ((b3 * b2) * q))) + (((a3 * c1) * r) + ((b3 * c2) * r))) + (((a3 * d1) * s) + ((b3 * d2) * s))) by RLVECT_1:def 6

        .= ((((((a3 * a1) + (b3 * a2)) * p) + (((a3 * b1) + (b3 * b2)) * q)) + (((a3 * c1) * r) + ((b3 * c2) * r))) + (((a3 * d1) * s) + ((b3 * d2) * s))) by RLVECT_1:def 6

        .= ((((((a3 * a1) + (b3 * a2)) * p) + (((a3 * b1) + (b3 * b2)) * q)) + (((a3 * c1) + (b3 * c2)) * r)) + (((a3 * d1) * s) + ((b3 * d2) * s))) by RLVECT_1:def 6

        .= ((((((a3 * a1) + (b3 * a2)) * p) + (((a3 * b1) + (b3 * b2)) * q)) + (((a3 * c1) + (b3 * c2)) * r)) + (((a3 * d1) + (b3 * d2)) * s)) by RLVECT_1:def 6;

      end;



       A11: not r is zero by A2, Th2;

       A12:

      now

        assume

         A13: not are_Prop (u,v);

        ex w st ( not w is zero & (u,v,w) are_LinDep & ex A,B,C be Real st w = (((A * p) + (B * q)) + (C * r)))

        proof

           A14:

          now

            set a3 = ( - (d2 * (d1 " ))), b3 = 1, w = ((a3 * u) + (b3 * v));

            assume that

             A15: d1 <> 0 and

             A16: d2 <> 0 ;

            set A = ((a3 * a1) + (b3 * a2)), B = ((a3 * b1) + (b3 * b2)), C = ((a3 * c1) + (b3 * c2));



             A17: A <> 0 or B <> 0 or C <> 0

            proof



               A18: (d2 * (d1 " )) <> 0

              proof

                assume not thesis;

                then (d1 " ) = 0 by A16, XCMPLX_1: 6;

                hence contradiction by A15, XCMPLX_1: 202;

              end;



               A19: ((d2 * (d1 " )) * d1) = (d2 * ((d1 " ) * d1))

              .= (d2 * 1) by A15, XCMPLX_0:def 7

              .= d2;

              assume

               A20: not thesis;

              then

               A21: ( - ( - ((d2 * (d1 " )) * c1))) = c2;

              ( - ( - ((d2 * (d1 " )) * a1))) = a2 & ( - ( - ((d2 * (d1 " )) * b1))) = b2 by A20;

              then ((d2 * (d1 " )) * u) = v by A6, A9, A21, A19, Lm4;

              hence contradiction by A13, A18, ANPROJ_1: 1;

            end;

            ((a3 * d1) + (b3 * d2)) = (( - (d2 * ((d1 " ) * d1))) + d2)

            .= (( - (d2 * 1)) + d2) by A15, XCMPLX_0:def 7

            .= 0 ;



            then

             A22: w = ((((((a3 * a1) + (b3 * a2)) * p) + (((a3 * b1) + (b3 * b2)) * q)) + (((a3 * c1) + (b3 * c2)) * r)) + ( 0 * s)) by A10

            .= ((((((a3 * a1) + (b3 * a2)) * p) + (((a3 * b1) + (b3 * b2)) * q)) + (((a3 * c1) + (b3 * c2)) * r)) + ( 0. V)) by RLVECT_1: 10

            .= (((((a3 * a1) + (b3 * a2)) * p) + (((a3 * b1) + (b3 * b2)) * q)) + (((a3 * c1) + (b3 * c2)) * r)) by RLVECT_1: 4;



            then

             A23: w = ((((A * p) + (B * q)) + (C * r)) + ( 0. V)) by RLVECT_1: 4

            .= ((((A * p) + (B * q)) + (C * r)) + ( 0 * s)) by RLVECT_1: 10;



             A24: not w is zero by A2, A23, A17;

            (u,v,w) are_LinDep by A4, A5, A13, ANPROJ_1: 6;

            hence thesis by A22, A24;

          end;

           A25:

          now

            assume

             A26: d2 = 0 ;

            take w = v;



             A27: (u,v,w) are_LinDep by ANPROJ_1: 11;

            w = ((((a2 * p) + (b2 * q)) + (c2 * r)) + ( 0. V)) by A9, A26, RLVECT_1: 10

            .= (((a2 * p) + (b2 * q)) + (c2 * r)) by RLVECT_1: 4;

            hence thesis by A5, A27;

          end;

          now

            assume

             A28: d1 = 0 ;

            take w = u;



             A29: (u,v,w) are_LinDep by ANPROJ_1: 11;

            w = ((((a1 * p) + (b1 * q)) + (c1 * r)) + ( 0. V)) by A6, A28, RLVECT_1: 10

            .= (((a1 * p) + (b1 * q)) + (c1 * r)) by RLVECT_1: 4;

            hence thesis by A4, A29;

          end;

          hence thesis by A25, A14;

        end;

        then

        consider w such that

         A30: not w is zero and

         A31: (u,v,w) are_LinDep and

         A32: ex A,B,C be Real st w = (((A * p) + (B * q)) + (C * r));

        consider A,B,C be Real such that

         A33: w = (((A * p) + (B * q)) + (C * r)) by A32;

         A34:

        now

          set b = 1, a = ( - A);

          set y = ((a * p) + (b * w));



           A35: y = ((((a + (b * A)) * p) + ((b * B) * q)) + ((b * C) * r)) by A33, Lm7

          .= ((( 0. V) + ((1 * B) * q)) + ((1 * C) * r)) by RLVECT_1: 10

          .= ((B * q) + (C * r)) by RLVECT_1: 4;

          assume

           A36: not are_Prop (p,w);

          then

           A37: (p,w,y) are_LinDep by A3, A30, ANPROJ_1: 6;



           A38: B <> 0 or C <> 0

          proof

            assume not thesis;



            then

             A39: w = (((A * p) + ( 0. V)) + ( 0 * r)) by A33, RLVECT_1: 10

            .= (((A * p) + ( 0. V)) + ( 0. V)) by RLVECT_1: 10

            .= ((A * p) + ( 0. V)) by RLVECT_1: 4

            .= (A * p) by RLVECT_1: 4;

            A <> 0 by A39, RLVECT_1: 10, A30;

            hence contradiction by A36, A39, ANPROJ_1: 1;

          end;



           A40: not y is zero

          proof

            assume not thesis;



            then ( 0. V) = ((B * q) + (C * r)) by A35

            .= ((( 0. V) + (B * q)) + (C * r)) by RLVECT_1: 4

            .= ((( 0 * p) + (B * q)) + (C * r)) by RLVECT_1: 10

            .= (((( 0 * p) + (B * q)) + (C * r)) + ( 0. V)) by RLVECT_1: 4

            .= (((( 0 * p) + (B * q)) + (C * r)) + ( 0 * s)) by RLVECT_1: 10;

            hence contradiction by A2, A38;

          end;

          (q,r,y) are_LinDep by A8, A11, A7, A35, ANPROJ_1: 6;

          hence thesis by A30, A31, A40, A37;

        end;

        now

          assume are_Prop (p,w);

          then (q,r,q) are_LinDep & (p,w,q) are_LinDep by ANPROJ_1: 11;

          hence thesis by A8, A30, A31;

        end;

        hence thesis by A34;

      end;

      now

        assume are_Prop (u,v);

        then

         A41: (u,v,p) are_LinDep by ANPROJ_1: 11;

        (q,r,q) are_LinDep & (p,p,q) are_LinDep by ANPROJ_1: 11;

        hence thesis by A3, A8, A41;

      end;

      hence thesis by A12;

    end;

    theorem :: ANPROJ_2:5



     Th5: (for a, b, a1, b1 st ((((a * u) + (b * v)) + (a1 * u1)) + (b1 * v1)) = ( 0. V) holds a = 0 & b = 0 & a1 = 0 & b1 = 0 ) implies not ex y st not y is zero & (u,v,y) are_LinDep & (u1,v1,y) are_LinDep

    proof

      assume

       A1: for a, b, a1, b1 st ((((a * u) + (b * v)) + (a1 * u1)) + (b1 * v1)) = ( 0. V) holds a = 0 & b = 0 & a1 = 0 & b1 = 0 ;

      then

       A2: not are_Prop (u,v) by Th2;

      assume not thesis;

      then

      consider y such that

       A3: not y is zero and

       A4: (u,v,y) are_LinDep and

       A5: (u1,v1,y) are_LinDep ;

       not u is zero & not v is zero by A1, Th2;

      then

      consider a, b such that

       A6: y = ((a * u) + (b * v)) by A4, A2, ANPROJ_1: 6;



       A7: not are_Prop (u1,v1) by A1, Th2;

       not u1 is zero & not v1 is zero by A1, Th2;

      then

      consider a1, b1 such that

       A8: y = ((a1 * u1) + (b1 * v1)) by A5, A7, ANPROJ_1: 6;

      ( 0. V) = (((a * u) + (b * v)) - ((a1 * u1) + (b1 * v1))) by A6, A8, RLVECT_1: 15

      .= (((a * u) + (b * v)) + (( - 1) * ((a1 * u1) + (b1 * v1)))) by RLVECT_1: 16

      .= (((a * u) + (b * v)) + ((( - 1) * (a1 * u1)) + (( - 1) * (b1 * v1)))) by RLVECT_1:def 5

      .= (((a * u) + (b * v)) + (((( - 1) * a1) * u1) + (( - 1) * (b1 * v1)))) by RLVECT_1:def 7

      .= (((a * u) + (b * v)) + (((( - 1) * a1) * u1) + ((( - 1) * b1) * v1))) by RLVECT_1:def 7

      .= ((((a * u) + (b * v)) + ((( - 1) * a1) * u1)) + ((( - 1) * b1) * v1)) by RLVECT_1:def 3;

      then a = 0 & b = 0 by A1;



      then y = (( 0. V) + ( 0 * v)) by A6, RLVECT_1: 10

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

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

      hence contradiction by A3;

    end;

    definition

      let V, u, v, w;

      :: ANPROJ_2:def1

      pred u,v,w are_Prop_Vect means not u is zero & not v is zero & not w is zero;

    end

    definition

      let V, u, v, w, u1, v1, w1;

      :: ANPROJ_2:def2

      pred u,v,w,u1,v1,w1 lie_on_a_triangle means (u,v,w1) are_LinDep & (u,w,v1) are_LinDep & (v,w,u1) are_LinDep ;

    end

    definition

      let V, o, u, v, w, u2, v2, w2;

      :: ANPROJ_2:def3

      pred o,u,v,w,u2,v2,w2 are_perspective means (o,u,u2) are_LinDep & (o,v,v2) are_LinDep & (o,w,w2) are_LinDep ;

    end



     Lm8: ( - (a * o)) = (( - a) * o)

    proof



      thus ( - (a * o)) = (a * ( - o)) by RLVECT_1: 25

      .= (( - a) * o) by RLVECT_1: 24;

    end;

    theorem :: ANPROJ_2:6



     Th6: (o,u,u2) are_LinDep & not are_Prop (o,u) & not are_Prop (o,u2) & not are_Prop (u,u2) & (o,u,u2) are_Prop_Vect implies (ex a1, b1 st (b1 * u2) = (o + (a1 * u)) & a1 <> 0 & b1 <> 0 ) & ex a2, c2 st u2 = ((c2 * o) + (a2 * u)) & c2 <> 0 & a2 <> 0

    proof

      assume that

       A1: (o,u,u2) are_LinDep and

       A2: not are_Prop (o,u) and

       A3: not are_Prop (o,u2) and

       A4: not are_Prop (u,u2) and

       A5: (o,u,u2) are_Prop_Vect ;

      consider a, b, c such that

       A6: (((a * o) + (b * u)) + (c * u2)) = ( 0. V) and

       A7: a <> 0 or b <> 0 or c <> 0 by A1;

       not u is zero by A5;

      then

       A8: u <> ( 0. V);

       not u2 is zero by A5;

      then

       A9: u2 <> ( 0. V);

       not o is zero by A5;

      then

       A10: o <> ( 0. V);



       A11: a <> 0 & b <> 0 & c <> 0

      proof

         A12:

        now

          assume

           A13: b = 0 ;



          then ( 0. V) = (((a * o) + ( 0. V)) + (c * u2)) by A6, RLVECT_1: 10

          .= ((a * o) + (c * u2)) by RLVECT_1: 4;



          then (a * o) = ( - (c * u2)) by RLVECT_1: 6

          .= (c * ( - u2)) by RLVECT_1: 25;

          then

           A14: (a * o) = (( - c) * u2) by RLVECT_1: 24;



           A15: a <> 0 & c <> 0

          proof

             A16:

            now

              assume

               A17: c = 0 ;



              then ( 0. V) = (((a * o) + ( 0 * u)) + ( 0. V)) by A6, A13, RLVECT_1: 10

              .= ((a * o) + ( 0 * u)) by RLVECT_1: 4

              .= ((a * o) + ( 0. V)) by RLVECT_1: 10

              .= (a * o) by RLVECT_1: 4;

              hence contradiction by A7, A10, A13, A17, RLVECT_1: 11;

            end;

             A18:

            now

              assume

               A19: a = 0 ;



              then ( 0. V) = ((( 0. V) + ( 0 * u)) + (c * u2)) by A6, A13, RLVECT_1: 10

              .= (( 0 * u) + (c * u2)) by RLVECT_1: 4

              .= (( 0. V) + (c * u2)) by RLVECT_1: 10

              .= (c * u2) by RLVECT_1: 4;

              hence contradiction by A7, A9, A13, A19, RLVECT_1: 11;

            end;

            assume not thesis;

            hence contradiction by A18, A16;

          end;

          then ( - c) <> 0 ;

          hence contradiction by A3, A15, A14;

        end;

         A20:

        now

          assume

           A21: a = 0 ;



          then ( 0. V) = ((( 0. V) + (b * u)) + (c * u2)) by A6, RLVECT_1: 10

          .= ((b * u) + (c * u2)) by RLVECT_1: 4;



          then (b * u) = ( - (c * u2)) by RLVECT_1: 6

          .= (c * ( - u2)) by RLVECT_1: 25;

          then

           A22: (b * u) = (( - c) * u2) by RLVECT_1: 24;



           A23: b <> 0 & c <> 0

          proof

             A24:

            now

              assume

               A25: c = 0 ;



              then ( 0. V) = ((( 0. V) + (b * u)) + ( 0 * u2)) by A6, A21, RLVECT_1: 10

              .= ((b * u) + ( 0 * u2)) by RLVECT_1: 4

              .= ((b * u) + ( 0. V)) by RLVECT_1: 10

              .= (b * u) by RLVECT_1: 4;

              hence contradiction by A7, A8, A21, A25, RLVECT_1: 11;

            end;

             A26:

            now

              assume

               A27: b = 0 ;



              then ( 0. V) = ((( 0. V) + ( 0 * u)) + (c * u2)) by A6, A21, RLVECT_1: 10

              .= (( 0 * u) + (c * u2)) by RLVECT_1: 4

              .= (( 0. V) + (c * u2)) by RLVECT_1: 10

              .= (c * u2) by RLVECT_1: 4;

              hence contradiction by A7, A9, A21, A27, RLVECT_1: 11;

            end;

            assume not thesis;

            hence contradiction by A26, A24;

          end;

          then ( - c) <> 0 ;

          hence contradiction by A4, A23, A22;

        end;

         A28:

        now

          assume

           A29: c = 0 ;



          then ( 0. V) = (((a * o) + (b * u)) + ( 0. V)) by A6, RLVECT_1: 10

          .= ((a * o) + (b * u)) by RLVECT_1: 4;



          then (a * o) = ( - (b * u)) by RLVECT_1: 6

          .= (b * ( - u)) by RLVECT_1: 25;

          then

           A30: (a * o) = (( - b) * u) by RLVECT_1: 24;



           A31: a <> 0 & b <> 0

          proof

             A32:

            now

              assume

               A33: b = 0 ;



              then ( 0. V) = (((a * o) + ( 0 * u)) + ( 0. V)) by A6, A29, RLVECT_1: 10

              .= ((a * o) + ( 0 * u)) by RLVECT_1: 4

              .= ((a * o) + ( 0. V)) by RLVECT_1: 10

              .= (a * o) by RLVECT_1: 4;

              hence contradiction by A7, A10, A29, A33, RLVECT_1: 11;

            end;

             A34:

            now

              assume

               A35: a = 0 ;



              then ( 0. V) = ((( 0. V) + (b * u)) + ( 0 * u2)) by A6, A29, RLVECT_1: 10

              .= ((b * u) + ( 0 * u2)) by RLVECT_1: 4

              .= ((b * u) + ( 0. V)) by RLVECT_1: 10

              .= (b * u) by RLVECT_1: 4;

              hence contradiction by A7, A8, A29, A35, RLVECT_1: 11;

            end;

            assume not thesis;

            hence contradiction by A34, A32;

          end;

          then ( - b) <> 0 ;

          hence contradiction by A2, A31, A30;

        end;

        assume not thesis;

        hence contradiction by A20, A12, A28;

      end;

      then

       A36: (c " ) <> 0 by XCMPLX_1: 202;

      (a " ) <> 0 by A11, XCMPLX_1: 202;

      then

       A37: ((a " ) * b) <> 0 & ( - ((a " ) * c)) <> 0 by A11, XCMPLX_1: 6;

      ((a " ) * ( - (c * u2))) = ((a " ) * ((a * o) + (b * u))) by A6, RLVECT_1: 6

      .= (((a " ) * (a * o)) + ((a " ) * (b * u))) by RLVECT_1:def 5

      .= ((((a " ) * a) * o) + ((a " ) * (b * u))) by RLVECT_1:def 7

      .= ((((a " ) * a) * o) + (((a " ) * b) * u)) by RLVECT_1:def 7

      .= ((1 * o) + (((a " ) * b) * u)) by A11, XCMPLX_0:def 7

      .= (o + (((a " ) * b) * u)) by RLVECT_1:def 8;



      then (o + (((a " ) * b) * u)) = ((a " ) * (c * ( - u2))) by RLVECT_1: 25

      .= (((a " ) * c) * ( - u2)) by RLVECT_1:def 7

      .= (( - ((a " ) * c)) * u2) by RLVECT_1: 24;

      hence ex a1, b1 st (b1 * u2) = (o + (a1 * u)) & a1 <> 0 & b1 <> 0 by A37;

      ( - b) <> 0 by A11;

      then

       A38: ((c " ) * ( - b)) <> 0 by A36, XCMPLX_1: 6;

      (c * u2) = ( - ((a * o) + (b * u))) by A6, RLVECT_1:def 10

      .= (( - (a * o)) + ( - (b * u))) by RLVECT_1: 31

      .= ((( - a) * o) + ( - (b * u))) by Lm8

      .= ((( - a) * o) + (( - b) * u)) by Lm8;



      then ((c " ) * (c * u2)) = (((c " ) * (( - a) * o)) + ((c " ) * (( - b) * u))) by RLVECT_1:def 5

      .= ((((c " ) * ( - a)) * o) + ((c " ) * (( - b) * u))) by RLVECT_1:def 7

      .= ((((c " ) * ( - a)) * o) + (((c " ) * ( - b)) * u)) by RLVECT_1:def 7;



      then

       A39: ((((c " ) * ( - a)) * o) + (((c " ) * ( - b)) * u)) = (((c " ) * c) * u2) by RLVECT_1:def 7

      .= (1 * u2) by A11, XCMPLX_0:def 7

      .= u2 by RLVECT_1:def 8;

      ( - a) <> 0 by A11;

      then ((c " ) * ( - a)) <> 0 by A36, XCMPLX_1: 6;

      hence thesis by A39, A38;

    end;

    theorem :: ANPROJ_2:7



     Th7: (p,q,r) are_LinDep & not are_Prop (p,q) & (p,q,r) are_Prop_Vect implies ex a, b st r = ((a * p) + (b * q))

    proof

      assume that

       A1: (p,q,r) are_LinDep and

       A2: not are_Prop (p,q) and

       A3: (p,q,r) are_Prop_Vect ;

      consider a, b, c such that

       A4: (((a * p) + (b * q)) + (c * r)) = ( 0. V) and

       A5: a <> 0 or b <> 0 or c <> 0 by A1;

       not q is zero by A3;

      then

       A6: q <> ( 0. V);

       not p is zero by A3;

      then

       A7: p <> ( 0. V);



       A8: c <> 0

      proof

        assume

         A9: not thesis;



        then ( 0. V) = (((a * p) + (b * q)) + ( 0. V)) by A4, RLVECT_1: 10

        .= ((a * p) + (b * q)) by RLVECT_1: 4;



        then

         A10: (a * p) = ( - (b * q)) by RLVECT_1: 6

        .= (( - b) * q) by Lm8;



         A11: a <> 0 & b <> 0

        proof

           A12:

          now

            assume

             A13: b = 0 ;



            then ( 0. V) = (((a * p) + ( 0. V)) + ( 0 * r)) by A4, A9, RLVECT_1: 10

            .= (((a * p) + ( 0. V)) + ( 0. V)) by RLVECT_1: 10

            .= ((a * p) + ( 0. V)) by RLVECT_1: 4

            .= (a * p) by RLVECT_1: 4;

            hence contradiction by A7, A5, A9, A13, RLVECT_1: 11;

          end;

           A14:

          now

            assume

             A15: a = 0 ;



            then ( 0. V) = ((( 0. V) + (b * q)) + ( 0 * r)) by A4, A9, RLVECT_1: 10

            .= ((( 0. V) + (b * q)) + ( 0. V)) by RLVECT_1: 10

            .= ((b * q) + ( 0. V)) by RLVECT_1: 4

            .= (b * q) by RLVECT_1: 4;

            hence contradiction by A6, A5, A9, A15, RLVECT_1: 11;

          end;

          assume not thesis;

          hence contradiction by A14, A12;

        end;

        then ( - b) <> 0 ;

        hence contradiction by A2, A11, A10;

      end;

      (c * r) = ( - ((a * p) + (b * q))) by A4, RLVECT_1:def 10

      .= (( - (a * p)) + ( - (b * q))) by RLVECT_1: 31

      .= ((( - a) * p) + ( - (b * q))) by Lm8

      .= ((( - a) * p) + (( - b) * q)) by Lm8;



      then ((c " ) * (c * r)) = (((c " ) * (( - a) * p)) + ((c " ) * (( - b) * q))) by RLVECT_1:def 5

      .= ((((c " ) * ( - a)) * p) + ((c " ) * (( - b) * q))) by RLVECT_1:def 7

      .= ((((c " ) * ( - a)) * p) + (((c " ) * ( - b)) * q)) by RLVECT_1:def 7;



      then ((((c " ) * ( - a)) * p) + (((c " ) * ( - b)) * q)) = (((c " ) * c) * r) by RLVECT_1:def 7

      .= (1 * r) by A8, XCMPLX_0:def 7

      .= r by RLVECT_1:def 8;

      hence thesis;

    end;



     Lm9: (b1 * u2) = w2 & b1 <> 0 implies are_Prop (u2,w2)

    proof

      assume that

       A1: (b1 * u2) = w2 and

       A2: b1 <> 0 ;

      (b1 * u2) = (1 * w2) by A1, RLVECT_1:def 8;

      hence thesis by A2;

    end;



     Lm10: q = (o + (a * p)) & r = (o + (b * s)) & are_Prop (q,r) & a <> 0 implies (o,p,s) are_LinDep

    proof

      assume that

       A1: q = (o + (a * p)) & r = (o + (b * s)) & are_Prop (q,r) and

       A2: a <> 0 ;

      consider A be Real such that A <> 0 and

       A3: (o + (a * p)) = (A * (o + (b * s))) by A1, ANPROJ_1: 1;

      (o + (a * p)) = ((A * o) + (A * (b * s))) by A3, RLVECT_1:def 5

      .= ((A * o) + ((A * b) * s)) by RLVECT_1:def 7;



      then (( - (A * o)) + (o + (a * p))) = ((( - (A * o)) + (A * o)) + ((A * b) * s)) by RLVECT_1:def 3

      .= (( 0. V) + ((A * b) * s)) by RLVECT_1: 5

      .= ((A * b) * s) by RLVECT_1: 4;

      then ((( - (A * o)) + o) + (a * p)) = ((A * b) * s) by RLVECT_1:def 3;



      then ((A * b) * s) = (((( - A) * o) + o) + (a * p)) by Lm8

      .= (((( - A) * o) + (1 * o)) + (a * p)) by RLVECT_1:def 8

      .= (((( - A) + 1) * o) + (a * p)) by RLVECT_1:def 6;

      then ((((( - A) + 1) * o) + (a * p)) + ( - ((A * b) * s))) = ( 0. V) by RLVECT_1: 5;

      then ( 0. V) = ((((( - A) + 1) * o) + (a * p)) + (( - (A * b)) * s)) by Lm8;

      hence thesis by A2;

    end;



     Lm11: (a * p) = q & a <> 0 & not p is zero implies not q is zero by RLVECT_1: 11;



     Lm12: for A,B be Real holds (r = ((A * u2) + (B * v2)) & u2 = (o + (a1 * u)) & v2 = (o + (a2 * v)) implies r = ((((A + B) * o) + ((A * a1) * u)) + ((B * a2) * v)))

    proof

      let A,B be Real;

      assume r = ((A * u2) + (B * v2)) & u2 = (o + (a1 * u)) & v2 = (o + (a2 * v));



      hence r = (((A * o) + (A * (a1 * u))) + (B * (o + (a2 * v)))) by RLVECT_1:def 5

      .= (((A * o) + (A * (a1 * u))) + ((B * o) + (B * (a2 * v)))) by RLVECT_1:def 5

      .= (((A * o) + ((A * a1) * u)) + ((B * o) + (B * (a2 * v)))) by RLVECT_1:def 7

      .= (((A * o) + ((A * a1) * u)) + ((B * o) + ((B * a2) * v))) by RLVECT_1:def 7

      .= ((((A * o) + ((A * a1) * u)) + (B * o)) + ((B * a2) * v)) by RLVECT_1:def 3

      .= ((((A * o) + (B * o)) + ((A * a1) * u)) + ((B * a2) * v)) by RLVECT_1:def 3

      .= ((((A + B) * o) + ((A * a1) * u)) + ((B * a2) * v)) by RLVECT_1:def 6;

    end;



     Lm13: r = ((a * p) + (b * q)) implies r = ((( 0 * o) + (a * p)) + (b * q))

    proof

      assume r = ((a * p) + (b * q));



      hence r = ((( 0. V) + (a * p)) + (b * q)) by RLVECT_1: 4

      .= ((( 0 * o) + (a * p)) + (b * q)) by RLVECT_1: 10;

    end;



     Lm14: (( 0 * p) + ( 0 * q)) = ( 0. V)

    proof



      thus (( 0 * p) + ( 0 * q)) = (( 0. V) + ( 0 * q)) by RLVECT_1: 10

      .= ( 0 * q) by RLVECT_1: 4

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

    end;



     Lm15: ((( 0 * o) + ((b * a2) * v)) + ((( - b) * a3) * w)) = (b * ((a2 * v) - (a3 * w)))

    proof



      thus ((( 0 * o) + ((b * a2) * v)) + ((( - b) * a3) * w)) = ((( 0. V) + ((b * a2) * v)) + ((( - b) * a3) * w)) by RLVECT_1: 10

      .= (((b * a2) * v) + ((( - b) * a3) * w)) by RLVECT_1: 4

      .= ((b * (a2 * v)) + ((b * ( - a3)) * w)) by RLVECT_1:def 7

      .= ((b * (a2 * v)) + (b * (( - a3) * w))) by RLVECT_1:def 7

      .= ((b * (a2 * v)) + (b * ( - (a3 * w)))) by Lm8

      .= (b * ((a2 * v) - (a3 * w))) by RLVECT_1:def 5;

    end;

    theorem :: ANPROJ_2:8



     Th8: not o is zero & (u,v,w) are_Prop_Vect & (u2,v2,w2) are_Prop_Vect & (u1,v1,w1) are_Prop_Vect & (o,u,v,w,u2,v2,w2) are_perspective & not are_Prop (o,u2) & not are_Prop (o,v2) & not are_Prop (o,w2) & not are_Prop (u,u2) & not are_Prop (v,v2) & not are_Prop (w,w2) & not (o,u,v) are_LinDep & not (o,u,w) are_LinDep & not (o,v,w) are_LinDep & (u,v,w,u1,v1,w1) lie_on_a_triangle & (u2,v2,w2,u1,v1,w1) lie_on_a_triangle implies (u1,v1,w1) are_LinDep

    proof

      assume that

       A1: not o is zero and

       A2: (u,v,w) are_Prop_Vect and

       A3: (u2,v2,w2) are_Prop_Vect and

       A4: (u1,v1,w1) are_Prop_Vect and

       A5: (o,u,v,w,u2,v2,w2) are_perspective and

       A6: not are_Prop (o,u2) and

       A7: not are_Prop (o,v2) and

       A8: not are_Prop (o,w2) and

       A9: not are_Prop (u,u2) and

       A10: not are_Prop (v,v2) and

       A11: not are_Prop (w,w2) and

       A12: not (o,u,v) are_LinDep and

       A13: not (o,u,w) are_LinDep and

       A14: not (o,v,w) are_LinDep and

       A15: (u,v,w,u1,v1,w1) lie_on_a_triangle and

       A16: (u2,v2,w2,u1,v1,w1) lie_on_a_triangle ;



       A17: not w is zero by A2;



       A18: (o,w,w2) are_LinDep & not are_Prop (w,o) by A5, A13, ANPROJ_1: 11;



       A19: not w2 is zero by A3;

      then (o,w,w2) are_Prop_Vect by A1, A17;

      then

      consider a3, b3 such that

       A20: (b3 * w2) = (o + (a3 * w)) and a3 <> 0 and

       A21: b3 <> 0 by A8, A11, A18, Th6;



       A22: not u is zero by A2;



       A23: not v is zero by A2;



       A24: (o,v,v2) are_LinDep & not are_Prop (o,v) by A5, A12, ANPROJ_1: 11;



       A25: (o,u,u2) are_LinDep & not are_Prop (o,u) by A5, A12, ANPROJ_1: 11;



       A26: not u2 is zero by A3;

      then (o,u,u2) are_Prop_Vect by A1, A22;

      then

      consider a1, b1 such that

       A27: (b1 * u2) = (o + (a1 * u)) and

       A28: a1 <> 0 and

       A29: b1 <> 0 by A6, A9, A25, Th6;



       A30: not v2 is zero by A3;

      then (o,v,v2) are_Prop_Vect by A1, A23;

      then

      consider a2, b2 such that

       A31: (b2 * v2) = (o + (a2 * v)) and

       A32: a2 <> 0 and

       A33: b2 <> 0 by A7, A10, A24, Th6;

      set u29 = (o + (a1 * u)), v29 = (o + (a2 * v)), w29 = (o + (a3 * w));



       A34: are_Prop (v2,v29) by A31, A33, Lm9;



       A35: not v29 is zero by A30, A31, A33, Lm11;



       A36: are_Prop (w2,w29) by A20, A21, Lm9;



       A37: (u,v,w1) are_LinDep & not are_Prop (u,v) by A12, A15, ANPROJ_1: 12;



       A38: not w1 is zero by A4;

      then (u,v,w1) are_Prop_Vect by A22, A23;

      then

      consider c3, d3 such that

       A39: w1 = ((c3 * u) + (d3 * v)) by A37, Th7;



       A40: are_Prop (u2,u29) by A27, A29, Lm9;



       A41: (v,w,u1) are_LinDep & not are_Prop (v,w) by A14, A15, ANPROJ_1: 12;



       A42: not u1 is zero by A4;

      then (v,w,u1) are_Prop_Vect by A23, A17;

      then

      consider c1, d1 such that

       A43: u1 = ((c1 * v) + (d1 * w)) by A41, Th7;

      (v2,w2,u1) are_LinDep by A16;

      then

       A44: (v29,w29,u1) are_LinDep by A34, A36, ANPROJ_1: 4;



       A45: not are_Prop (v29,w29) by A14, A32, Lm10;



       A46: not w29 is zero by A19, A20, A21, Lm11;

      then (v29,w29,u1) are_Prop_Vect by A42, A35;

      then

      consider A1,B1 be Real such that

       A47: u1 = ((A1 * v29) + (B1 * w29)) by A44, A45, Th7;



       A48: (u,w,v1) are_LinDep & not are_Prop (u,w) by A13, A15, ANPROJ_1: 12;



       A49: not v1 is zero by A4;

      then (u,w,v1) are_Prop_Vect by A22, A17;

      then

      consider c2, d2 such that

       A50: v1 = ((c2 * u) + (d2 * w)) by A48, Th7;



       A51: u1 = ((((A1 + B1) * o) + ((A1 * a2) * v)) + ((B1 * a3) * w)) by A47, Lm12;

      (u2,v2,w1) are_LinDep by A16;

      then

       A52: (u29,v29,w1) are_LinDep by A40, A34, ANPROJ_1: 4;



       A53: not are_Prop (u29,v29) by A12, A28, Lm10;



       A54: not u29 is zero by A26, A27, A29, Lm11;

      then (u29,v29,w1) are_Prop_Vect by A38, A35;

      then

      consider A3,B3 be Real such that

       A55: w1 = ((A3 * u29) + (B3 * v29)) by A52, A53, Th7;

      (u2,w2,v1) are_LinDep by A16;

      then

       A56: (u29,w29,v1) are_LinDep by A40, A36, ANPROJ_1: 4;



       A57: not are_Prop (u29,w29) by A13, A28, Lm10;



       A58: w1 = ((((A3 + B3) * o) + ((A3 * a1) * u)) + ((B3 * a2) * v)) by A55, Lm12;

      (u29,w29,v1) are_Prop_Vect by A49, A54, A46;

      then

      consider A2,B2 be Real such that

       A59: v1 = ((A2 * u29) + (B2 * w29)) by A56, A57, Th7;



       A60: v1 = ((((A2 + B2) * o) + ((A2 * a1) * u)) + ((B2 * a3) * w)) by A59, Lm12;

      w1 = ((( 0 * o) + (c3 * u)) + (d3 * v)) by A39, Lm13;

      then

       A61: (A3 + B3) = 0 by A12, A58, ANPROJ_1: 8;

      u1 = ((( 0 * o) + (c1 * v)) + (d1 * w)) by A43, Lm13;

      then

       A62: (A1 + B1) = 0 by A14, A51, ANPROJ_1: 8;

      v1 = ((( 0 * o) + (c2 * u)) + (d2 * w)) by A50, Lm13;

      then

       A63: (A2 + B2) = 0 by A13, A60, ANPROJ_1: 8;

      then

       A64: A1 <> 0 & A2 <> 0 & A3 <> 0 by A42, A47, A62, A49, A59, A38, A55, A61, Lm14;

      set u19 = ((a2 * v) - (a3 * w)), v19 = ((a1 * u) - (a3 * w)), w19 = ((a1 * u) - (a2 * v));

      B1 = ( - A1) by A62;

      then u1 = (A1 * u19) by A51, Lm15;

      then

       A65: are_Prop (u19,u1) by A64, Lm9;

      B3 = ( - A3) by A61;

      then w1 = (A3 * w19) by A58, Lm15;

      then

       A66: are_Prop (w19,w1) by A64, Lm9;

      B2 = ( - A2) by A63;

      then v1 = (A2 * v19) by A60, Lm15;

      then

       A67: are_Prop (v19,v1) by A64, Lm9;

      (((1 * u19) + (( - 1) * v19)) + (1 * w19)) = ((u19 + (( - 1) * v19)) + (1 * w19)) by RLVECT_1:def 8

      .= ((u19 + (( - 1) * v19)) + w19) by RLVECT_1:def 8

      .= ((u19 + ( - v19)) + w19) by RLVECT_1: 16

      .= ((((a2 * v) + ( - (a3 * w))) + ((a3 * w) + ( - (a1 * u)))) + ((a1 * u) - (a2 * v))) by RLVECT_1: 33

      .= (((((a2 * v) + ( - (a3 * w))) + (a3 * w)) + ( - (a1 * u))) + ((a1 * u) + ( - (a2 * v)))) by RLVECT_1:def 3

      .= ((((a2 * v) + (( - (a3 * w)) + (a3 * w))) + ( - (a1 * u))) + ((a1 * u) + ( - (a2 * v)))) by RLVECT_1:def 3

      .= ((((a2 * v) + ( 0. V)) + ( - (a1 * u))) + ((a1 * u) + ( - (a2 * v)))) by RLVECT_1: 5

      .= (((a2 * v) + ( - (a1 * u))) + ((a1 * u) + ( - (a2 * v)))) by RLVECT_1: 4

      .= ((a2 * v) + (( - (a1 * u)) + ((a1 * u) + ( - (a2 * v))))) by RLVECT_1:def 3

      .= ((a2 * v) + ((( - (a1 * u)) + (a1 * u)) + ( - (a2 * v)))) by RLVECT_1:def 3

      .= ((a2 * v) + (( 0. V) + ( - (a2 * v)))) by RLVECT_1: 5

      .= ((a2 * v) + ( - (a2 * v))) by RLVECT_1: 4

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

      then (u19,v19,w19) are_LinDep ;

      hence thesis by A65, A67, A66, ANPROJ_1: 4;

    end;

    definition

      let V, o, u, v, w, u2, v2, w2;

      :: ANPROJ_2:def4

      pred o,u,v,w,u2,v2,w2 lie_on_an_angle means not (o,u,u2) are_LinDep & (o,u,v) are_LinDep & (o,u,w) are_LinDep & (o,u2,v2) are_LinDep & (o,u2,w2) are_LinDep ;

    end

    definition

      let V, o, u, v, w, u2, v2, w2;

      :: ANPROJ_2:def5

      pred o,u,v,w,u2,v2,w2 are_half_mutually_not_Prop means not are_Prop (o,v) & not are_Prop (o,w) & not are_Prop (o,v2) & not are_Prop (o,w2) & not are_Prop (u,v) & not are_Prop (u,w) & not are_Prop (u2,v2) & not are_Prop (u2,w2) & not are_Prop (v,w) & not are_Prop (v2,w2);

    end



     Lm16: (b1 * u2) = w2 & b1 <> 0 implies are_Prop (u2,w2)

    proof

      assume that

       A1: (b1 * u2) = w2 and

       A2: b1 <> 0 ;

      (b1 * u2) = (1 * w2) by A1, RLVECT_1:def 8;

      hence thesis by A2;

    end;



     Lm17: not are_Prop (p,q) & y = (a * q) & a <> 0 implies not are_Prop (p,y)

    proof

      assume that

       A1: not are_Prop (p,q) and

       A2: y = (a * q) & a <> 0 ;

      assume not thesis;

      then

      consider b such that

       A3: b <> 0 & p = (b * y) by ANPROJ_1: 1;

      p = ((b * a) * q) & (b * a) <> 0 by A2, A3, RLVECT_1:def 7, XCMPLX_1: 6;

      hence contradiction by A1, ANPROJ_1: 1;

    end;



     Lm18: w1 = ((a * u) + (b * v2)) & v2 = (o + (c2 * u2)) implies w1 = (((b * o) + (a * u)) + ((b * c2) * u2))

    proof

      assume w1 = ((a * u) + (b * v2)) & v2 = (o + (c2 * u2));



      hence w1 = ((a * u) + ((b * o) + (b * (c2 * u2)))) by RLVECT_1:def 5

      .= (((a * u) + (b * o)) + (b * (c2 * u2))) by RLVECT_1:def 3

      .= (((b * o) + (a * u)) + ((b * c2) * u2)) by RLVECT_1:def 7;

    end;



     Lm19: w1 = ((a * u2) + (b * v1)) & v1 = (o + (a2 * u)) implies w1 = (((b * o) + ((b * a2) * u)) + (a * u2))

    proof

      assume w1 = ((a * u2) + (b * v1)) & v1 = (o + (a2 * u));



      hence w1 = (((b * o) + (a * u2)) + ((b * a2) * u)) by Lm18

      .= (((b * o) + ((b * a2) * u)) + (a * u2)) by RLVECT_1:def 3;

    end;



     Lm20: (a * p) = q & a <> 0 & not p is zero implies not q is zero by RLVECT_1: 11;



     Lm21: not are_Prop (p,q) & y = (a * q) & a <> 0 & s = (b * p) & b <> 0 implies not are_Prop (s,y)

    proof

      assume that

       A1: not are_Prop (p,q) and

       A2: y = (a * q) & a <> 0 and

       A3: s = (b * p) & b <> 0 ;

      assume not thesis;

      then

      consider c such that

       A4: c <> 0 & s = (c * y) by ANPROJ_1: 1;

      s = ((c * a) * q) & (c * a) <> 0 by A2, A4, RLVECT_1:def 7, XCMPLX_1: 6;

      hence contradiction by A1, A3;

    end;



     Lm22: for A,B be Real holds (r = ((A * u2) + (B * v2)) & u2 = (o + (a1 * u)) & v2 = (o + (a2 * v)) implies r = ((((A + B) * o) + ((A * a1) * u)) + ((B * a2) * v)))

    proof

      let A,B be Real;

      assume r = ((A * u2) + (B * v2)) & u2 = (o + (a1 * u)) & v2 = (o + (a2 * v));



      hence r = (((A * o) + (A * (a1 * u))) + (B * (o + (a2 * v)))) by RLVECT_1:def 5

      .= (((A * o) + (A * (a1 * u))) + ((B * o) + (B * (a2 * v)))) by RLVECT_1:def 5

      .= (((A * o) + ((A * a1) * u)) + ((B * o) + (B * (a2 * v)))) by RLVECT_1:def 7

      .= (((A * o) + ((A * a1) * u)) + ((B * o) + ((B * a2) * v))) by RLVECT_1:def 7

      .= ((((A * o) + ((A * a1) * u)) + (B * o)) + ((B * a2) * v)) by RLVECT_1:def 3

      .= ((((A * o) + (B * o)) + ((A * a1) * u)) + ((B * a2) * v)) by RLVECT_1:def 3

      .= ((((A + B) * o) + ((A * a1) * u)) + ((B * a2) * v)) by RLVECT_1:def 6;

    end;



     Lm23: a2 <> a3 & c2 <> 0 implies ((a3 * c2) - (a2 * c2)) <> 0

    proof

      assume that

       A1: a2 <> a3 and

       A2: c2 <> 0 ;

      ((a3 * c2) - (a2 * c2)) = ((a3 - a2) * c2) & (a3 - a2) <> 0 by A1;

      hence thesis by A2, XCMPLX_1: 6;

    end;



     Lm24: for A1,A19,B1,B19 be Real holds ((A1 + B1) = (A19 + B19) & (A1 * a2) = (A19 * a3) & (B1 * c3) = (B19 * c2) & a2 <> a3 & c2 <> 0 implies A1 = ((((a3 * c3) - (a3 * c2)) * (((a3 * c2) - (a2 * c2)) " )) * B1))

    proof

      let A1,A19,B1,B19 be Real;

      assume that

       A1: (A1 + B1) = (A19 + B19) and

       A2: (A1 * a2) = (A19 * a3) & (B1 * c3) = (B19 * c2) and

       A3: a2 <> a3 & c2 <> 0 ;



       A4: ((A1 * (a3 * c2)) + (B1 * (a3 * c2))) = ((A19 + B19) * (a3 * c2)) by A1, XCMPLX_1: 8;

      (A1 * (a2 * c2)) = ((A19 * a3) * c2) & (B1 * (c3 * a3)) = ((B19 * c2) * a3) by A2, XCMPLX_1: 4;

      then (B1 * ((a3 * c3) - (a3 * c2))) = (A1 * ((a3 * c2) - (a2 * c2))) by A4;

      then

       A5: (A1 * (((a3 * c2) - (a2 * c2)) * (((a3 * c2) - (a2 * c2)) " ))) = ((B1 * ((a3 * c3) - (a3 * c2))) * (((a3 * c2) - (a2 * c2)) " )) by XCMPLX_1: 4;

      ((a3 * c2) - (a2 * c2)) <> 0 by A3, Lm23;

      then (A1 * 1) = ((B1 * ((a3 * c3) - (a3 * c2))) * (((a3 * c2) - (a2 * c2)) " )) by A5, XCMPLX_0:def 7;

      hence thesis;

    end;



     Lm25: for B1 be Real st c2 <> 0 & a2 <> a3 & B1 <> 0 holds (B1 * (((a3 * c2) - (a2 * c2)) " )) <> 0

    proof

      let B1 be Real;

      assume that

       A1: c2 <> 0 & a2 <> a3 and

       A2: B1 <> 0 ;

      (((a3 * c2) - (a2 * c2)) " ) <> 0 by A1, Lm23, XCMPLX_1: 202;

      hence thesis by A2, XCMPLX_1: 6;

    end;



     Lm26: for A1,B1 be Real holds (A1 = ((((a3 * c3) - (a3 * c2)) * (((a3 * c2) - (a2 * c2)) " )) * B1) & c2 <> 0 & a2 <> a3 & u1 = ((((A1 + B1) * o) + ((A1 * a2) * u)) + ((B1 * c3) * u2)) implies u1 = ((B1 * (((a3 * c2) - (a2 * c2)) " )) * (((((a3 * c3) - (a2 * c2)) * o) + (((a2 * a3) * (c3 - c2)) * u)) + (((c2 * c3) * (a3 - a2)) * u2))))

    proof

      let A1,B1 be Real;

      assume that

       A1: A1 = ((((a3 * c3) - (a3 * c2)) * (((a3 * c2) - (a2 * c2)) " )) * B1) and

       A2: c2 <> 0 & a2 <> a3 and

       A3: u1 = ((((A1 + B1) * o) + ((A1 * a2) * u)) + ((B1 * c3) * u2));



       A4: ((a3 * c2) - (a2 * c2)) <> 0 by A2, Lm23;



       A5: ((B1 * c3) * u2) = (((B1 * 1) * c3) * u2)

      .= (((B1 * ((((a3 * c2) - (a2 * c2)) " ) * ((a3 * c2) - (a2 * c2)))) * c3) * u2) by A4, XCMPLX_0:def 7

      .= (((B1 * (((a3 * c2) - (a2 * c2)) " )) * ((c3 * c2) * (a3 - a2))) * u2)

      .= ((B1 * (((a3 * c2) - (a2 * c2)) " )) * (((c2 * c3) * (a3 - a2)) * u2)) by RLVECT_1:def 7;



       A6: ((((((a3 * c3) - (a3 * c2)) * (((a3 * c2) - (a2 * c2)) " )) * B1) * a2) * u) = (((B1 * (((a3 * c2) - (a2 * c2)) " )) * ((a2 * a3) * (c3 - c2))) * u)

      .= ((B1 * (((a3 * c2) - (a2 * c2)) " )) * (((a2 * a3) * (c3 - c2)) * u)) by RLVECT_1:def 7;

      ((((((a3 * c3) - (a3 * c2)) * (((a3 * c2) - (a2 * c2)) " )) * B1) + (B1 * 1)) * o) = (((((a3 * c3) - (a3 * c2)) * (B1 * (((a3 * c2) - (a2 * c2)) " ))) + (B1 * ((((a3 * c2) - (a2 * c2)) " ) * ((a3 * c2) - (a2 * c2))))) * o) by A4, XCMPLX_0:def 7

      .= (((B1 * (((a3 * c2) - (a2 * c2)) " )) * ((((a3 * c3) + ( - (a3 * c2))) + (a3 * c2)) - (a2 * c2))) * o)

      .= ((B1 * (((a3 * c2) - (a2 * c2)) " )) * (((a3 * c3) - (a2 * c2)) * o)) by RLVECT_1:def 7;



      hence u1 = (((B1 * (((a3 * c2) - (a2 * c2)) " )) * ((((a3 * c3) - (a2 * c2)) * o) + (((a2 * a3) * (c3 - c2)) * u))) + ((B1 * (((a3 * c2) - (a2 * c2)) " )) * (((c2 * c3) * (a3 - a2)) * u2))) by A1, A3, A6, A5, RLVECT_1:def 5

      .= ((B1 * (((a3 * c2) - (a2 * c2)) " )) * (((((a3 * c3) - (a2 * c2)) * o) + (((a2 * a3) * (c3 - c2)) * u)) + (((c2 * c3) * (a3 - a2)) * u2))) by RLVECT_1:def 5;

    end;



     Lm27: (((p + q) + r) + ((u + u2) + u1)) = (((p + u) + (q + u2)) + (r + u1))

    proof



      thus (((p + u) + (q + u2)) + (r + u1)) = ((u + (p + (q + u2))) + (r + u1)) by RLVECT_1:def 3

      .= ((u + ((p + q) + u2)) + (r + u1)) by RLVECT_1:def 3

      .= (((u + u2) + (p + q)) + (r + u1)) by RLVECT_1:def 3

      .= ((u + u2) + ((p + q) + (r + u1))) by RLVECT_1:def 3

      .= ((u + u2) + (((p + q) + r) + u1)) by RLVECT_1:def 3

      .= (((p + q) + r) + ((u + u2) + u1)) by RLVECT_1:def 3;

    end;



     Lm28: for C2,C3 be Real holds (u1 = (((((a3 * c3) - (a2 * c2)) * o) + (((a2 * a3) * (c3 - c2)) * u)) + (((c2 * c3) * (a3 - a2)) * u2)) & v1 = ((o + (a3 * u)) + (c3 * u2)) & w2 = ((o + (a2 * u)) + (c2 * u2)) & (C2 + C3) = ((a2 * c2) - (a3 * c3)) & ((C2 * a3) + (C3 * a2)) = ((a2 * a3) * (c2 - c3)) & ((C2 * c3) + (C3 * c2)) = ((c2 * c3) * (a2 - a3)) implies (((1 * u1) + (C2 * v1)) + (C3 * w2)) = ( 0. V))

    proof

      let C2,C3 be Real such that

       A1: u1 = (((((a3 * c3) - (a2 * c2)) * o) + (((a2 * a3) * (c3 - c2)) * u)) + (((c2 * c3) * (a3 - a2)) * u2)) and

       A2: v1 = ((o + (a3 * u)) + (c3 * u2)) & w2 = ((o + (a2 * u)) + (c2 * u2)) and

       A3: (C2 + C3) = ((a2 * c2) - (a3 * c3)) & ((C2 * a3) + (C3 * a2)) = ((a2 * a3) * (c2 - c3)) & ((C2 * c3) + (C3 * c2)) = ((c2 * c3) * (a2 - a3));



       A4: (((1 * u1) + (C2 * v1)) + (C3 * w2)) = ((u1 + (C2 * v1)) + (C3 * w2)) by RLVECT_1:def 8

      .= (u1 + ((C2 * v1) + (C3 * w2))) by RLVECT_1:def 3;

      ((C2 * v1) + (C3 * w2)) = (((C2 * (o + (a3 * u))) + (C2 * (c3 * u2))) + (C3 * ((o + (a2 * u)) + (c2 * u2)))) by A2, RLVECT_1:def 5

      .= ((((C2 * o) + (C2 * (a3 * u))) + (C2 * (c3 * u2))) + (C3 * ((o + (a2 * u)) + (c2 * u2)))) by RLVECT_1:def 5

      .= ((((C2 * o) + (C2 * (a3 * u))) + (C2 * (c3 * u2))) + ((C3 * (o + (a2 * u))) + (C3 * (c2 * u2)))) by RLVECT_1:def 5

      .= ((((C2 * o) + (C2 * (a3 * u))) + (C2 * (c3 * u2))) + (((C3 * o) + (C3 * (a2 * u))) + (C3 * (c2 * u2)))) by RLVECT_1:def 5

      .= ((((C2 * o) + (C3 * o)) + ((C2 * (a3 * u)) + (C3 * (a2 * u)))) + ((C2 * (c3 * u2)) + (C3 * (c2 * u2)))) by Lm27

      .= ((((C2 + C3) * o) + ((C2 * (a3 * u)) + (C3 * (a2 * u)))) + ((C2 * (c3 * u2)) + (C3 * (c2 * u2)))) by RLVECT_1:def 6

      .= ((((C2 + C3) * o) + (((C2 * a3) * u) + (C3 * (a2 * u)))) + ((C2 * (c3 * u2)) + (C3 * (c2 * u2)))) by RLVECT_1:def 7

      .= ((((C2 + C3) * o) + (((C2 * a3) * u) + ((C3 * a2) * u))) + ((C2 * (c3 * u2)) + (C3 * (c2 * u2)))) by RLVECT_1:def 7

      .= ((((C2 + C3) * o) + (((C2 * a3) * u) + ((C3 * a2) * u))) + (((C2 * c3) * u2) + (C3 * (c2 * u2)))) by RLVECT_1:def 7

      .= ((((C2 + C3) * o) + (((C2 * a3) * u) + ((C3 * a2) * u))) + (((C2 * c3) * u2) + ((C3 * c2) * u2))) by RLVECT_1:def 7

      .= ((((C2 + C3) * o) + (((C2 * a3) + (C3 * a2)) * u)) + (((C2 * c3) * u2) + ((C3 * c2) * u2))) by RLVECT_1:def 6

      .= (((((a2 * c2) - (a3 * c3)) * o) + (((a2 * a3) * (c2 - c3)) * u)) + (((c2 * c3) * (a2 - a3)) * u2)) by A3, RLVECT_1:def 6;



      hence (((1 * u1) + (C2 * v1)) + (C3 * w2)) = ((((((a3 * c3) - (a2 * c2)) * o) + (((a2 * c2) - (a3 * c3)) * o)) + ((((a2 * a3) * (c3 - c2)) * u) + (((a2 * a3) * (c2 - c3)) * u))) + ((((c2 * c3) * (a3 - a2)) * u2) + (((c2 * c3) * (a2 - a3)) * u2))) by A1, A4, Lm27

      .= ((((((a3 * c3) - (a2 * c2)) + ((a2 * c2) - (a3 * c3))) * o) + ((((a2 * a3) * (c3 - c2)) * u) + (((a2 * a3) * (c2 - c3)) * u))) + ((((c2 * c3) * (a3 - a2)) * u2) + (((c2 * c3) * (a2 - a3)) * u2))) by RLVECT_1:def 6

      .= ((((((a3 * c3) - (a2 * c2)) + ((a2 * c2) - (a3 * c3))) * o) + ((((a2 * a3) * (c3 - c2)) + ((a2 * a3) * (c2 - c3))) * u)) + ((((c2 * c3) * (a3 - a2)) * u2) + (((c2 * c3) * (a2 - a3)) * u2))) by RLVECT_1:def 6

      .= (((((((a3 * c3) + ( - (a2 * c2))) + (a2 * c2)) + ( - (a3 * c3))) * o) + ((((a2 * a3) * (c3 - c2)) + ((a2 * a3) * (c2 - c3))) * u)) + ((((c2 * c3) * (a3 - a2)) + ((c2 * c3) * (a2 - a3))) * u2)) by RLVECT_1:def 6

      .= ((( 0. V) + ((((a2 * a3) * (c3 - c2)) + ((a2 * a3) * (c2 - c3))) * u)) + ((((c2 * c3) * (a3 - a2)) + ((c2 * c3) * (a2 - a3))) * u2)) by RLVECT_1: 10

      .= (( 0 * u) + ((((c2 * c3) * (a3 - a2)) + ( - ((c2 * c3) * (a3 - a2)))) * u2)) by RLVECT_1: 4

      .= (( 0. V) + ( 0 * u2)) by RLVECT_1: 10

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

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

    end;



     Lm29: for A3,A39,B3,B39 be Real holds (w2 = ((o + (a2 * u)) + (c2 * u2)) & w1 = (((B3 * o) + (A3 * u)) + ((B3 * c2) * u2)) & B3 = B39 & A3 = (B39 * a2) implies w1 = (B3 * w2))

    proof

      let A3,A39,B3,B39 be Real;

      assume that

       A1: w2 = ((o + (a2 * u)) + (c2 * u2)) and

       A2: w1 = (((B3 * o) + (A3 * u)) + ((B3 * c2) * u2)) & B3 = B39 & A3 = (B39 * a2);



      thus w1 = (((B3 * o) + (B3 * (a2 * u))) + ((B3 * c2) * u2)) by A2, RLVECT_1:def 7

      .= (((B3 * o) + (B3 * (a2 * u))) + (B3 * (c2 * u2))) by RLVECT_1:def 7

      .= ((B3 * (o + (a2 * u))) + (B3 * (c2 * u2))) by RLVECT_1:def 5

      .= (B3 * w2) by A1, RLVECT_1:def 5;

    end;

    theorem :: ANPROJ_2:9



     Th9: not o is zero & (u,v,w) are_Prop_Vect & (u2,v2,w2) are_Prop_Vect & (u1,v1,w1) are_Prop_Vect & (o,u,v,w,u2,v2,w2) lie_on_an_angle & (o,u,v,w,u2,v2,w2) are_half_mutually_not_Prop & (u,v2,w1) are_LinDep & (u2,v,w1) are_LinDep & (u,w2,v1) are_LinDep & (w,u2,v1) are_LinDep & (v,w2,u1) are_LinDep & (w,v2,u1) are_LinDep implies (u1,v1,w1) are_LinDep

    proof

      assume that

       A1: not o is zero and

       A2: (u,v,w) are_Prop_Vect and

       A3: (u2,v2,w2) are_Prop_Vect and

       A4: (u1,v1,w1) are_Prop_Vect and

       A5: (o,u,v,w,u2,v2,w2) lie_on_an_angle and

       A6: (o,u,v,w,u2,v2,w2) are_half_mutually_not_Prop and

       A7: (u,v2,w1) are_LinDep and

       A8: (u2,v,w1) are_LinDep and

       A9: (u,w2,v1) are_LinDep and

       A10: (w,u2,v1) are_LinDep and

       A11: (v,w2,u1) are_LinDep and

       A12: (w,v2,u1) are_LinDep ;



       A13: not u is zero by A2;



       A14: not are_Prop (u2,v2) by A6;



       A15: not are_Prop (o,v) by A6;



       A16: not are_Prop (u,v) by A6;



       A17: (o,u2,v2) are_LinDep by A5;



       A18: ( not are_Prop (o,w2)) & not are_Prop (u2,w2) by A6;



       A19: not u2 is zero by A3;



       A20: ( not are_Prop (o,w)) & not are_Prop (u,w) by A6;



       A21: (o,u,w) are_LinDep by A5;



       A22: not are_Prop (o,v2) by A6;



       A23: (o,u2,w2) are_LinDep by A5;



       A24: not (o,u,u2) are_LinDep by A5;

      then

       A25: not are_Prop (o,u) by ANPROJ_1: 12;



       A26: not w is zero by A2;

      then (o,u,w) are_Prop_Vect by A1, A13;

      then

      consider a3, b3 such that

       A27: (b3 * w) = (o + (a3 * u)) and a3 <> 0 and

       A28: b3 <> 0 by A21, A20, A25, Th6;



       A29: not are_Prop (u2,o) by A24, ANPROJ_1: 12;



       A30: not w2 is zero by A3;

      then (o,u2,w2) are_Prop_Vect by A1, A19;

      then

      consider c3, d3 such that

       A31: (d3 * w2) = (o + (c3 * u2)) and c3 <> 0 and

       A32: d3 <> 0 by A23, A18, A29, Th6;



       A33: (o,u,v) are_LinDep by A5;



       A34: not v2 is zero by A3;

      then (o,u2,v2) are_Prop_Vect by A1, A19;

      then

      consider c2, d2 such that

       A35: (d2 * v2) = (o + (c2 * u2)) and

       A36: c2 <> 0 and

       A37: d2 <> 0 by A17, A22, A14, A29, Th6;



       A38: not v is zero by A2;

      then (o,u,v) are_Prop_Vect by A1, A13;

      then

      consider a2, b2 such that

       A39: (b2 * v) = (o + (a2 * u)) and a2 <> 0 and

       A40: b2 <> 0 by A33, A15, A16, A25, Th6;

      set v9 = (o + (a2 * u)), w9 = (o + (a3 * u)), v29 = (o + (c2 * u2)), w29 = (o + (c3 * u2));



       A41: not v29 is zero by A34, A35, A37, Lm20;



       A42: not v9 is zero by A38, A39, A40, Lm20;



       A43: not w9 is zero by A26, A27, A28, Lm20;



       A44: not w29 is zero by A30, A31, A32, Lm20;



       A45: are_Prop (w2,w29) by A31, A32, Lm16;

      then

       A46: (u,w29,v1) are_LinDep by A9, ANPROJ_1: 4;



       A47: are_Prop (v,v9) by A39, A40, Lm16;

      then

       A48: (v9,w29,u1) are_LinDep by A11, A45, ANPROJ_1: 4;



       A49: are_Prop (v2,v29) by A35, A37, Lm16;

      then

       A50: (u,v29,w1) are_LinDep by A7, ANPROJ_1: 4;



       A51: are_Prop (w,w9) by A27, A28, Lm16;

      then

       A52: (w9,v29,u1) are_LinDep by A12, A49, ANPROJ_1: 4;

       not are_Prop (u,v2)

      proof

        assume not thesis;

        then (o,u2,u) are_LinDep by A17, ANPROJ_1: 4;

        hence contradiction by A24, ANPROJ_1: 5;

      end;

      then not are_Prop (u,v29) by A35, A37, Lm17;

      then

      consider A3,B3 be Real such that

       A53: w1 = ((A3 * u) + (B3 * v29)) by A13, A50, A41, ANPROJ_1: 6;

       not (o,u2,v) are_LinDep

      proof

        assume not thesis;

        then

         A54: (o,v,u2) are_LinDep by ANPROJ_1: 5;

        (o,v,u) are_LinDep & (o,v,o) are_LinDep by A33, ANPROJ_1: 5, ANPROJ_1: 11;

        hence contradiction by A1, A38, A24, A15, A54, ANPROJ_1: 14;

      end;

      then not are_Prop (v,w2) by A23, ANPROJ_1: 4;

      then not are_Prop (v9,w29) by A39, A40, A31, A32, Lm21;

      then

      consider A1,B1 be Real such that

       A55: u1 = ((A1 * v9) + (B1 * w29)) by A42, A44, A48, ANPROJ_1: 6;

       not (o,u,v2) are_LinDep

      proof

        assume not thesis;

        then

         A56: (o,v2,u) are_LinDep by ANPROJ_1: 5;

        (o,v2,u2) are_LinDep & (o,v2,o) are_LinDep by A17, ANPROJ_1: 5, ANPROJ_1: 11;

        hence contradiction by A1, A34, A24, A22, A56, ANPROJ_1: 14;

      end;

      then not are_Prop (v2,w) by A21, ANPROJ_1: 4;

      then not are_Prop (w9,v29) by A27, A28, A35, A37, Lm21;

      then

      consider A19,B19 be Real such that

       A57: u1 = ((A19 * w9) + (B19 * v29)) by A41, A43, A52, ANPROJ_1: 6;



       A58: u1 = ((((A1 + B1) * o) + ((A1 * a2) * u)) + ((B1 * c3) * u2)) by A55, Lm22;



       A59: not are_Prop (v2,w2) by A6;



       A60: not are_Prop (v,w) by A6;



       A61: not are_Prop (v9,w9) & not are_Prop (v29,w29)

      proof

         A62:

        now

          assume are_Prop (v29,w29);

          then are_Prop (v2,w29) by A49, ANPROJ_1: 2;

          hence contradiction by A59, A45, ANPROJ_1: 2;

        end;

         A63:

        now

          assume are_Prop (v9,w9);

          then are_Prop (v,w9) by A47, ANPROJ_1: 2;

          hence contradiction by A60, A51, ANPROJ_1: 2;

        end;

        assume not thesis;

        hence contradiction by A63, A62;

      end;

       not are_Prop (u,w2)

      proof

        assume not thesis;

        then (o,u2,u) are_LinDep by A23, ANPROJ_1: 4;

        hence contradiction by A24, ANPROJ_1: 5;

      end;

      then not are_Prop (u,w29) by A31, A32, Lm17;

      then

      consider A2,B2 be Real such that

       A64: v1 = ((A2 * u) + (B2 * w29)) by A13, A44, A46, ANPROJ_1: 6;

      (u2,w,v1) are_LinDep by A10;

      then

       A65: (u2,w9,v1) are_LinDep by A51, ANPROJ_1: 4;

       not are_Prop (u2,w) by A24, A21, ANPROJ_1: 4;

      then not are_Prop (u2,w9) by A27, A28, Lm17;

      then

      consider A29,B29 be Real such that

       A66: v1 = ((A29 * u2) + (B29 * w9)) by A19, A43, A65, ANPROJ_1: 6;



       A67: v1 = (((B2 * o) + (A2 * u)) + ((B2 * c3) * u2)) by A64, Lm18;



       A68: (u2,v9,w1) are_LinDep by A8, A47, ANPROJ_1: 4;

       not are_Prop (u2,v) by A24, A33, ANPROJ_1: 4;

      then not are_Prop (u2,v9) by A39, A40, Lm17;

      then

      consider A39,B39 be Real such that

       A69: w1 = ((A39 * u2) + (B39 * v9)) by A19, A68, A42, ANPROJ_1: 6;



       A70: w1 = (((B3 * o) + (A3 * u)) + ((B3 * c2) * u2)) by A53, Lm18;

      v1 = (((B29 * o) + ((B29 * a3) * u)) + (A29 * u2)) by A66, Lm19;

      then

       A71: B2 = B29 & A2 = (B29 * a3) by A24, A67, ANPROJ_1: 8;

      w1 = (((B39 * o) + ((B39 * a2) * u)) + (A39 * u2)) by A69, Lm19;

      then

       A72: B3 = B39 & A3 = (B39 * a2) by A24, A70, ANPROJ_1: 8;



       A73: u1 = ((((A19 + B19) * o) + ((A19 * a3) * u)) + ((B19 * c2) * u2)) by A57, Lm22;

      then

       A74: (B1 * c3) = (B19 * c2) by A24, A58, ANPROJ_1: 8;

      (A1 + B1) = (A19 + B19) & (A1 * a2) = (A19 * a3) by A24, A58, A73, ANPROJ_1: 8;

      then

       A75: A1 = ((((a3 * c3) - (a3 * c2)) * (((a3 * c2) - (a2 * c2)) " )) * B1) by A36, A61, A74, Lm24;

      set v19 = ((o + (a3 * u)) + (c3 * u2));

      set C2 = (a2 * c2), C3 = ( - (a3 * c3));

      set u19 = (((((a3 * c3) - (a2 * c2)) * o) + (((a2 * a3) * (c3 - c2)) * u)) + (((c2 * c3) * (a3 - a2)) * u2));

      set w19 = ((o + (a2 * u)) + (c2 * u2));



       A76: ((C2 * c3) + (C3 * c2)) = ((c2 * c3) * (a2 - a3));

      (C2 + C3) = ((a2 * c2) - (a3 * c3)) & ((C2 * a3) + (C3 * a2)) = ((a2 * a3) * (c2 - c3));

      then (((1 * u19) + (C2 * v19)) + (C3 * w19)) = ( 0. V) by A76, Lm28;

      then

       A77: (u19,v19,w19) are_LinDep ;



       A78: not v1 is zero by A4;



       A79: B2 <> 0

      proof

        assume not thesis;



        then v1 = (( 0. V) + ( 0 * w29)) by A64, A71, RLVECT_1: 10

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

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

        hence contradiction by A78;

      end;

      v1 = (B2 * v19) by A67, A71, Lm29;

      then

       A80: are_Prop (v19,v1) by A79, Lm16;



       A81: not w1 is zero by A4;



       A82: B3 <> 0

      proof

        assume not thesis;



        then w1 = (( 0. V) + ( 0 * v29)) by A53, A72, RLVECT_1: 10

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

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

        hence contradiction by A81;

      end;

      w1 = (B3 * w19) by A70, A72, Lm29;

      then

       A83: are_Prop (w19,w1) by A82, Lm16;



       A84: not u1 is zero by A4;



       A85: B1 <> 0

      proof

        assume not thesis;



        then u1 = (( 0. V) + ( 0 * w29)) by A55, A75, RLVECT_1: 10

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

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

        hence contradiction by A84;

      end;

      u1 = ((B1 * (((a3 * c2) - (a2 * c2)) " )) * (((((a3 * c3) - (a2 * c2)) * o) + (((a2 * a3) * (c3 - c2)) * u)) + (((c2 * c3) * (a3 - a2)) * u2))) by A36, A61, A58, A75, Lm26;

      then are_Prop (u19,u1) by A36, A61, A85, Lm16, Lm25;

      hence thesis by A83, A80, A77, ANPROJ_1: 4;

    end;

    reserve A for non empty set;

    reserve f,g,h,f1 for Element of ( Funcs (A, REAL ));

    reserve x1,x2,x3,x4 for Element of A;

    theorem :: ANPROJ_2:10



     Th10: ex f st (f . x1) = 1 & for z st z in A & z <> x1 holds (f . z) = 0

    proof

      deffunc G( object) = ( In ( 0 , REAL ));

      deffunc F( object) = 1;

      defpred P[ object] means $1 = x1;



       A1: for z be object st z in A holds ( P[z] implies F(z) in REAL ) & ( not P[z] implies G(z) in REAL ) by XREAL_0:def 1;

      consider f be Function of A, REAL such that

       A2: for z be object st z in A holds ( P[z] implies (f . z) = F(z)) & ( not P[z] implies (f . z) = G(z)) from FUNCT_2:sch 5( A1);

      reconsider f as Element of ( Funcs (A, REAL )) by FUNCT_2: 8;

      take f;

      thus thesis by A2;

    end;

    theorem :: ANPROJ_2:11



     Th11: x1 <> x2 & x1 <> x3 & x2 <> x3 & (f . x1) = 1 & (for z st z in A holds (z <> x1 implies (f . z) = 0 )) & (g . x2) = 1 & (for z st z in A holds (z <> x2 implies (g . z) = 0 )) & (h . x3) = 1 & (for z st z in A holds (z <> x3 implies (h . z) = 0 )) implies for a,b,c be Real st (( RealFuncAdd A) . ((( RealFuncAdd A) . ((( RealFuncExtMult A) . [a, f]),(( RealFuncExtMult A) . [b, g]))),(( RealFuncExtMult A) . [c, h]))) = ( RealFuncZero A) holds a = 0 & b = 0 & c = 0

    proof

      set RM = ( RealFuncExtMult A), RA = ( RealFuncAdd A);

      assume that

       A1: x1 <> x2 and

       A2: x1 <> x3 and

       A3: x2 <> x3 and

       A4: (f . x1) = 1 and

       A5: for z st z in A holds (z <> x1 implies (f . z) = 0 ) and

       A6: (g . x2) = 1 and

       A7: for z st z in A holds (z <> x2 implies (g . z) = 0 ) and

       A8: (h . x3) = 1 and

       A9: for z st z in A holds (z <> x3 implies (h . z) = 0 );



       A10: (f . x2) = 0 & (h . x2) = 0 by A1, A3, A5, A9;

      let a,b,c be Real;

      assume

       A11: (RA . ((RA . ((RM . [a, f]),(RM . [b, g]))),(RM . [c, h]))) = ( RealFuncZero A);

      reconsider a, b, c as Element of REAL by XREAL_0:def 1;



       A12: 0 = ((RA . ((RA . ((RM . [a, f]),(RM . [b, g]))),(RM . [c, h]))) . x2) by FUNCOP_1: 7, A11

      .= (((RA . ((RM . [a, f]),(RM . [b, g]))) . x2) + ((RM . [c, h]) . x2)) by FUNCSDOM: 1

      .= ((((RM . [a, f]) . x2) + ((RM . [b, g]) . x2)) + ((RM . [c, h]) . x2)) by FUNCSDOM: 1

      .= ((((RM . [a, f]) . x2) + ((RM . [b, g]) . x2)) + (c * (h . x2))) by FUNCSDOM: 4

      .= ((((RM . [a, f]) . x2) + (b * (g . x2))) + (c * (h . x2))) by FUNCSDOM: 4

      .= (((a * 0 ) + (b * 1)) + (c * 0 )) by A6, A10, FUNCSDOM: 4

      .= b;



       A13: (g . x1) = 0 & (h . x1) = 0 by A1, A2, A7, A9;



       A14: (f . x3) = 0 & (g . x3) = 0 by A2, A3, A5, A7;



       A15: 0 = ((RA . ((RA . ((RM . [a, f]),(RM . [b, g]))),(RM . [c, h]))) . x3) by A11, FUNCOP_1: 7

      .= (((RA . ((RM . [a, f]),(RM . [b, g]))) . x3) + ((RM . [c, h]) . x3)) by FUNCSDOM: 1

      .= ((((RM . [a, f]) . x3) + ((RM . [b, g]) . x3)) + ((RM . [c, h]) . x3)) by FUNCSDOM: 1

      .= ((((RM . [a, f]) . x3) + ((RM . [b, g]) . x3)) + (c * (h . x3))) by FUNCSDOM: 4

      .= ((((RM . [a, f]) . x3) + (b * (g . x3))) + (c * (h . x3))) by FUNCSDOM: 4

      .= (((a * 0 ) + (b * 0 )) + (c * 1)) by A8, A14, FUNCSDOM: 4

      .= c;

       0 = ((RA . ((RA . ((RM . [a, f]),(RM . [b, g]))),(RM . [c, h]))) . x1) by A11, FUNCOP_1: 7

      .= (((RA . ((RM . [a, f]),(RM . [b, g]))) . x1) + ((RM . [c, h]) . x1)) by FUNCSDOM: 1

      .= ((((RM . [a, f]) . x1) + ((RM . [b, g]) . x1)) + ((RM . [c, h]) . x1)) by FUNCSDOM: 1

      .= ((((RM . [a, f]) . x1) + ((RM . [b, g]) . x1)) + (c * (h . x1))) by FUNCSDOM: 4

      .= ((((RM . [a, f]) . x1) + (b * (g . x1))) + (c * (h . x1))) by FUNCSDOM: 4

      .= (((a * 1) + (b * 0 )) + (c * 0 )) by A4, A13, FUNCSDOM: 4

      .= a;

      hence thesis by A12, A15;

    end;

    theorem :: ANPROJ_2:12

    x1 <> x2 & x1 <> x3 & x2 <> x3 implies ex f, g, h st for a,b,c be Real st (( RealFuncAdd A) . ((( RealFuncAdd A) . ((( RealFuncExtMult A) . [a, f]),(( RealFuncExtMult A) . [b, g]))),(( RealFuncExtMult A) . [c, h]))) = ( RealFuncZero A) holds a = 0 & b = 0 & c = 0

    proof

      assume

       A1: x1 <> x2 & x1 <> x3 & x2 <> x3;

      consider f such that

       A2: (f . x1) = 1 & for z st z in A holds (z <> x1 implies (f . z) = 0 ) by Th10;

      consider h such that

       A3: (h . x3) = 1 & for z st z in A holds (z <> x3 implies (h . z) = 0 ) by Th10;

      consider g such that

       A4: (g . x2) = 1 & for z st z in A holds (z <> x2 implies (g . z) = 0 ) by Th10;

      take f, g, h;

      let a,b,c be Real;

      assume (( RealFuncAdd A) . ((( RealFuncAdd A) . ((( RealFuncExtMult A) . [a, f]),(( RealFuncExtMult A) . [b, g]))),(( RealFuncExtMult A) . [c, h]))) = ( RealFuncZero A);

      hence thesis by A1, A2, A4, A3, Th11;

    end;

    theorem :: ANPROJ_2:13



     Th13: A = {x1, x2, x3} & x1 <> x2 & x1 <> x3 & x2 <> x3 & (f . x1) = 1 & (for z st z in A holds (z <> x1 implies (f . z) = 0 )) & (g . x2) = 1 & (for z st z in A holds (z <> x2 implies (g . z) = 0 )) & (h . x3) = 1 & (for z st z in A holds (z <> x3 implies (h . z) = 0 )) implies for h9 be Element of ( Funcs (A, REAL )) holds ex a,b,c be Real st h9 = (( RealFuncAdd A) . ((( RealFuncAdd A) . ((( RealFuncExtMult A) . [a, f]),(( RealFuncExtMult A) . [b, g]))),(( RealFuncExtMult A) . [c, h])))

    proof

      assume that

       A1: A = {x1, x2, x3} and

       A2: x1 <> x2 and

       A3: x1 <> x3 and

       A4: x2 <> x3 and

       A5: (f . x1) = 1 and

       A6: for z st z in A holds (z <> x1 implies (f . z) = 0 ) and

       A7: (g . x2) = 1 and

       A8: for z st z in A holds (z <> x2 implies (g . z) = 0 ) and

       A9: (h . x3) = 1 and

       A10: for z st z in A holds (z <> x3 implies (h . z) = 0 );



       A11: (g . x1) = 0 & (h . x1) = 0 by A2, A3, A8, A10;



       A12: (f . x2) = 0 & (h . x2) = 0 by A2, A4, A6, A10;

      let h9 be Element of ( Funcs (A, REAL ));

      take a = (h9 . x1), b = (h9 . x2), c = (h9 . x3);



       A13: (f . x3) = 0 & (g . x3) = 0 by A3, A4, A6, A8;

      now

        let x be Element of A;



         A14: x = x1 or x = x2 or x = x3 by A1, ENUMSET1:def 1;



         A15: ((( RealFuncAdd A) . ((( RealFuncAdd A) . ((( RealFuncExtMult A) . [a, f]),(( RealFuncExtMult A) . [b, g]))),(( RealFuncExtMult A) . [c, h]))) . x2) = (((( RealFuncAdd A) . ((( RealFuncExtMult A) . [a, f]),(( RealFuncExtMult A) . [b, g]))) . x2) + ((( RealFuncExtMult A) . [c, h]) . x2)) by FUNCSDOM: 1

        .= ((((( RealFuncExtMult A) . [a, f]) . x2) + ((( RealFuncExtMult A) . [b, g]) . x2)) + ((( RealFuncExtMult A) . [c, h]) . x2)) by FUNCSDOM: 1

        .= ((((( RealFuncExtMult A) . [a, f]) . x2) + ((( RealFuncExtMult A) . [b, g]) . x2)) + (c * (h . x2))) by FUNCSDOM: 4

        .= ((((( RealFuncExtMult A) . [a, f]) . x2) + (b * (g . x2))) + (c * (h . x2))) by FUNCSDOM: 4

        .= (((a * 0 ) + (b * 1)) + (c * 0 )) by A7, A12, FUNCSDOM: 4

        .= (h9 . x2);



         A16: ((( RealFuncAdd A) . ((( RealFuncAdd A) . ((( RealFuncExtMult A) . [a, f]),(( RealFuncExtMult A) . [b, g]))),(( RealFuncExtMult A) . [c, h]))) . x3) = (((( RealFuncAdd A) . ((( RealFuncExtMult A) . [a, f]),(( RealFuncExtMult A) . [b, g]))) . x3) + ((( RealFuncExtMult A) . [c, h]) . x3)) by FUNCSDOM: 1

        .= ((((( RealFuncExtMult A) . [a, f]) . x3) + ((( RealFuncExtMult A) . [b, g]) . x3)) + ((( RealFuncExtMult A) . [c, h]) . x3)) by FUNCSDOM: 1

        .= ((((( RealFuncExtMult A) . [a, f]) . x3) + ((( RealFuncExtMult A) . [b, g]) . x3)) + (c * (h . x3))) by FUNCSDOM: 4

        .= ((((( RealFuncExtMult A) . [a, f]) . x3) + (b * (g . x3))) + (c * (h . x3))) by FUNCSDOM: 4

        .= (((a * 0 ) + (b * 0 )) + (c * 1)) by A9, A13, FUNCSDOM: 4

        .= (h9 . x3);

        ((( RealFuncAdd A) . ((( RealFuncAdd A) . ((( RealFuncExtMult A) . [a, f]),(( RealFuncExtMult A) . [b, g]))),(( RealFuncExtMult A) . [c, h]))) . x1) = (((( RealFuncAdd A) . ((( RealFuncExtMult A) . [a, f]),(( RealFuncExtMult A) . [b, g]))) . x1) + ((( RealFuncExtMult A) . [c, h]) . x1)) by FUNCSDOM: 1

        .= ((((( RealFuncExtMult A) . [a, f]) . x1) + ((( RealFuncExtMult A) . [b, g]) . x1)) + ((( RealFuncExtMult A) . [c, h]) . x1)) by FUNCSDOM: 1

        .= ((((( RealFuncExtMult A) . [a, f]) . x1) + ((( RealFuncExtMult A) . [b, g]) . x1)) + (c * (h . x1))) by FUNCSDOM: 4

        .= ((((( RealFuncExtMult A) . [a, f]) . x1) + (b * (g . x1))) + (c * (h . x1))) by FUNCSDOM: 4

        .= (((a * 1) + (b * 0 )) + (c * 0 )) by A5, A11, FUNCSDOM: 4

        .= (h9 . x1);

        hence (h9 . x) = ((( RealFuncAdd A) . ((( RealFuncAdd A) . ((( RealFuncExtMult A) . [a, f]),(( RealFuncExtMult A) . [b, g]))),(( RealFuncExtMult A) . [c, h]))) . x) by A14, A15, A16;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: ANPROJ_2:14

    A = {x1, x2, x3} & x1 <> x2 & x1 <> x3 & x2 <> x3 implies ex f, g, h st for h9 be Element of ( Funcs (A, REAL )) holds ex a,b,c be Real st h9 = (( RealFuncAdd A) . ((( RealFuncAdd A) . ((( RealFuncExtMult A) . [a, f]),(( RealFuncExtMult A) . [b, g]))),(( RealFuncExtMult A) . [c, h])))

    proof

      assume

       A1: A = {x1, x2, x3} & x1 <> x2 & x1 <> x3 & x2 <> x3;

      consider f such that

       A2: (f . x1) = 1 & for z st z in A holds (z <> x1 implies (f . z) = 0 ) by Th10;

      consider h such that

       A3: (h . x3) = 1 & for z st z in A holds (z <> x3 implies (h . z) = 0 ) by Th10;

      consider g such that

       A4: (g . x2) = 1 & for z st z in A holds (z <> x2 implies (g . z) = 0 ) by Th10;

      take f, g, h;

      let h9 be Element of ( Funcs (A, REAL ));

      thus thesis by A1, A2, A4, A3, Th13;

    end;

    theorem :: ANPROJ_2:15



     Th15: A = {x1, x2, x3} & x1 <> x2 & x1 <> x3 & x2 <> x3 implies ex f, g, h st (for a,b,c be Real st (( RealFuncAdd A) . ((( RealFuncAdd A) . ((( RealFuncExtMult A) . [a, f]),(( RealFuncExtMult A) . [b, g]))),(( RealFuncExtMult A) . [c, h]))) = ( RealFuncZero A) holds a = 0 & b = 0 & c = 0 ) & for h9 be Element of ( Funcs (A, REAL )) holds ex a,b,c be Real st h9 = (( RealFuncAdd A) . ((( RealFuncAdd A) . ((( RealFuncExtMult A) . [a, f]),(( RealFuncExtMult A) . [b, g]))),(( RealFuncExtMult A) . [c, h])))

    proof

      assume

       A1: A = {x1, x2, x3} & x1 <> x2 & x1 <> x3 & x2 <> x3;

      consider f such that

       A2: (f . x1) = 1 & for z st z in A holds (z <> x1 implies (f . z) = 0 ) by Th10;

      consider h such that

       A3: (h . x3) = 1 & for z st z in A holds (z <> x3 implies (h . z) = 0 ) by Th10;

      consider g such that

       A4: (g . x2) = 1 & for z st z in A holds (z <> x2 implies (g . z) = 0 ) by Th10;

      take f, g, h;

      thus thesis by A1, A2, A4, A3, Th11, Th13;

    end;



     Lm30: ex A, x1, x2, x3 st A = {x1, x2, x3} & x1 <> x2 & x1 <> x3 & x2 <> x3

    proof

      reconsider A = { 0 , 1, 2} as non empty set;

      take A;

      reconsider x1 = 0 , x2 = 1, x3 = 2 as Element of A by ENUMSET1:def 1;

      take x1, x2, x3;

      thus thesis;

    end;

    theorem :: ANPROJ_2:16



     Th16: ex V be non trivial RealLinearSpace st ex u,v,w be Element of V st (for a, b, c st (((a * u) + (b * v)) + (c * w)) = ( 0. V) holds a = 0 & b = 0 & c = 0 ) & for y be Element of V holds ex a, b, c st y = (((a * u) + (b * v)) + (c * w))

    proof

      consider A, x1, x2, x3 such that

       A1: A = {x1, x2, x3} & x1 <> x2 & x1 <> x3 & x2 <> x3 by Lm30;

      set V = ( RealVectSpace A);

      consider f, g, h such that

       A2: for a,b,c be Real st (( RealFuncAdd A) . ((( RealFuncAdd A) . ((( RealFuncExtMult A) . [a, f]),(( RealFuncExtMult A) . [b, g]))),(( RealFuncExtMult A) . [c, h]))) = ( RealFuncZero A) holds a = 0 & b = 0 & c = 0 and

       A3: for h9 be Element of ( Funcs (A, REAL )) holds ex a,b,c be Real st h9 = (( RealFuncAdd A) . ((( RealFuncAdd A) . ((( RealFuncExtMult A) . [a, f]),(( RealFuncExtMult A) . [b, g]))),(( RealFuncExtMult A) . [c, h]))) by A1, Th15;

      reconsider u = f, v = g, w = h as Element of V;

      for a, b, c st (((a * u) + (b * v)) + (c * w)) = ( 0. V) holds a = 0 & b = 0 & c = 0 by A2;

      then not u is zero by Th1;

      then

       A4: u <> ( 0. V);



       A5: for y be Element of V holds ex a, b, c st y = (((a * u) + (b * v)) + (c * w))

      proof

        let y be Element of V;

        reconsider h9 = y as Element of ( Funcs (A, REAL ));

        consider a,b,c be Real such that

         A6: h9 = (( RealFuncAdd A) . ((( RealFuncAdd A) . ((( RealFuncExtMult A) . [a, f]),(( RealFuncExtMult A) . [b, g]))),(( RealFuncExtMult A) . [c, h]))) by A3;

        h9 = (((a * u) + (b * v)) + (c * w)) by A6;

        hence thesis;

      end;

      reconsider V as non trivial RealLinearSpace by A4, STRUCT_0:def 18;

      take V;

      reconsider u, v, w as Element of V;

      take u, v, w;

      thus for a, b, c st (((a * u) + (b * v)) + (c * w)) = ( 0. V) holds a = 0 & b = 0 & c = 0 by A2;

      let y be Element of V;

      ex a, b, c st y = (((a * u) + (b * v)) + (c * w)) by A5;

      hence thesis;

    end;

    theorem :: ANPROJ_2:17



     Th17: x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 & (f . x1) = 1 & (for z st z in A holds (z <> x1 implies (f . z) = 0 )) & (g . x2) = 1 & (for z st z in A holds (z <> x2 implies (g . z) = 0 )) & (h . x3) = 1 & (for z st z in A holds (z <> x3 implies (h . z) = 0 )) & (f1 . x4) = 1 & (for z st z in A holds (z <> x4 implies (f1 . z) = 0 )) implies for a,b,c,d be Real st (( RealFuncAdd A) . ((( RealFuncAdd A) . ((( RealFuncAdd A) . ((( RealFuncExtMult A) . [a, f]),(( RealFuncExtMult A) . [b, g]))),(( RealFuncExtMult A) . [c, h]))),(( RealFuncExtMult A) . [d, f1]))) = ( RealFuncZero A) holds a = 0 & b = 0 & c = 0 & d = 0

    proof

      set RM = ( RealFuncExtMult A), RA = ( RealFuncAdd A);

      assume that

       A1: x1 <> x2 and

       A2: x1 <> x3 and

       A3: x1 <> x4 and

       A4: x2 <> x3 and

       A5: x2 <> x4 and

       A6: x3 <> x4 and

       A7: (f . x1) = 1 and

       A8: for z st z in A holds (z <> x1 implies (f . z) = 0 ) and

       A9: (g . x2) = 1 and

       A10: for z st z in A holds (z <> x2 implies (g . z) = 0 ) and

       A11: (h . x3) = 1 and

       A12: for z st z in A holds (z <> x3 implies (h . z) = 0 ) and

       A13: (f1 . x4) = 1 and

       A14: for z st z in A holds (z <> x4 implies (f1 . z) = 0 );



       A15: (f . x2) = 0 & (h . x2) = 0 by A1, A4, A8, A12;



       A16: (g . x1) = 0 & (h . x1) = 0 by A1, A2, A10, A12;



       A17: (f1 . x1) = 0 by A3, A14;



       A18: (f1 . x2) = 0 by A5, A14;

      let a,b,c,d be Real;

      assume

       A19: (RA . ((RA . ((RA . ((RM . [a, f]),(RM . [b, g]))),(RM . [c, h]))),(RM . [d, f1]))) = ( RealFuncZero A);

      reconsider a, b, c, d as Element of REAL by XREAL_0:def 1;



       A20: 0 = ((RA . ((RA . ((RA . ((RM . [a, f]),(RM . [b, g]))),(RM . [c, h]))),(RM . [d, f1]))) . x2) by FUNCOP_1: 7, A19

      .= (((RA . ((RA . ((RM . [a, f]),(RM . [b, g]))),(RM . [c, h]))) . x2) + ((RM . [d, f1]) . x2)) by FUNCSDOM: 1

      .= ((((RA . ((RM . [a, f]),(RM . [b, g]))) . x2) + ((RM . [c, h]) . x2)) + ((RM . [d, f1]) . x2)) by FUNCSDOM: 1

      .= (((((RM . [a, f]) . x2) + ((RM . [b, g]) . x2)) + ((RM . [c, h]) . x2)) + ((RM . [d, f1]) . x2)) by FUNCSDOM: 1

      .= (((((RM . [a, f]) . x2) + ((RM . [b, g]) . x2)) + ((RM . [c, h]) . x2)) + (d * (f1 . x2))) by FUNCSDOM: 4

      .= (((((RM . [a, f]) . x2) + ((RM . [b, g]) . x2)) + (c * (h . x2))) + (d * (f1 . x2))) by FUNCSDOM: 4

      .= (((((RM . [a, f]) . x2) + (b * (g . x2))) + (c * (h . x2))) + (d * (f1 . x2))) by FUNCSDOM: 4

      .= ((((a * 0 ) + (b * 1)) + (c * 0 )) + (d * 0 )) by A9, A15, A18, FUNCSDOM: 4

      .= b;



       A21: (f . x4) = 0 & (g . x4) = 0 by A3, A5, A8, A10;



       A22: (h . x4) = 0 by A6, A12;



       A23: (f . x3) = 0 & (g . x3) = 0 by A2, A4, A8, A10;



       A24: (f1 . x3) = 0 by A6, A14;



       A25: 0 = ((RA . ((RA . ((RA . ((RM . [a, f]),(RM . [b, g]))),(RM . [c, h]))),(RM . [d, f1]))) . x4) by A19, FUNCOP_1: 7

      .= (((RA . ((RA . ((RM . [a, f]),(RM . [b, g]))),(RM . [c, h]))) . x4) + ((RM . [d, f1]) . x4)) by FUNCSDOM: 1

      .= ((((RA . ((RM . [a, f]),(RM . [b, g]))) . x4) + ((RM . [c, h]) . x4)) + ((RM . [d, f1]) . x4)) by FUNCSDOM: 1

      .= (((((RM . [a, f]) . x4) + ((RM . [b, g]) . x4)) + ((RM . [c, h]) . x4)) + ((RM . [d, f1]) . x4)) by FUNCSDOM: 1

      .= (((((RM . [a, f]) . x4) + ((RM . [b, g]) . x4)) + ((RM . [c, h]) . x4)) + (d * (f1 . x4))) by FUNCSDOM: 4

      .= (((((RM . [a, f]) . x4) + ((RM . [b, g]) . x4)) + (c * (h . x4))) + (d * (f1 . x4))) by FUNCSDOM: 4

      .= (((((RM . [a, f]) . x4) + (b * (g . x4))) + (c * (h . x4))) + (d * (f1 . x4))) by FUNCSDOM: 4

      .= ((((a * 0 ) + (b * 0 )) + (c * 0 )) + (d * 1)) by A13, A21, A22, FUNCSDOM: 4

      .= d;



       A26: 0 = ((RA . ((RA . ((RA . ((RM . [a, f]),(RM . [b, g]))),(RM . [c, h]))),(RM . [d, f1]))) . x3) by A19, FUNCOP_1: 7

      .= (((RA . ((RA . ((RM . [a, f]),(RM . [b, g]))),(RM . [c, h]))) . x3) + ((RM . [d, f1]) . x3)) by FUNCSDOM: 1

      .= ((((RA . ((RM . [a, f]),(RM . [b, g]))) . x3) + ((RM . [c, h]) . x3)) + ((RM . [d, f1]) . x3)) by FUNCSDOM: 1

      .= (((((RM . [a, f]) . x3) + ((RM . [b, g]) . x3)) + ((RM . [c, h]) . x3)) + ((RM . [d, f1]) . x3)) by FUNCSDOM: 1

      .= (((((RM . [a, f]) . x3) + ((RM . [b, g]) . x3)) + ((RM . [c, h]) . x3)) + (d * (f1 . x3))) by FUNCSDOM: 4

      .= (((((RM . [a, f]) . x3) + ((RM . [b, g]) . x3)) + (c * (h . x3))) + (d * (f1 . x3))) by FUNCSDOM: 4

      .= (((((RM . [a, f]) . x3) + (b * (g . x3))) + (c * (h . x3))) + (d * (f1 . x3))) by FUNCSDOM: 4

      .= ((((a * 0 ) + (b * 0 )) + (c * 1)) + (d * 0 )) by A11, A23, A24, FUNCSDOM: 4

      .= c;

       0 = ((RA . ((RA . ((RA . ((RM . [a, f]),(RM . [b, g]))),(RM . [c, h]))),(RM . [d, f1]))) . x1) by A19, FUNCOP_1: 7

      .= (((RA . ((RA . ((RM . [a, f]),(RM . [b, g]))),(RM . [c, h]))) . x1) + ((RM . [d, f1]) . x1)) by FUNCSDOM: 1

      .= ((((RA . ((RM . [a, f]),(RM . [b, g]))) . x1) + ((RM . [c, h]) . x1)) + ((RM . [d, f1]) . x1)) by FUNCSDOM: 1

      .= (((((RM . [a, f]) . x1) + ((RM . [b, g]) . x1)) + ((RM . [c, h]) . x1)) + ((RM . [d, f1]) . x1)) by FUNCSDOM: 1

      .= (((((RM . [a, f]) . x1) + ((RM . [b, g]) . x1)) + ((RM . [c, h]) . x1)) + (d * (f1 . x1))) by FUNCSDOM: 4

      .= (((((RM . [a, f]) . x1) + ((RM . [b, g]) . x1)) + (c * (h . x1))) + (d * (f1 . x1))) by FUNCSDOM: 4

      .= (((((RM . [a, f]) . x1) + (b * (g . x1))) + (c * (h . x1))) + (d * (f1 . x1))) by FUNCSDOM: 4

      .= ((((a * 1) + (b * 0 )) + (c * 0 )) + (d * 0 )) by A7, A16, A17, FUNCSDOM: 4

      .= a;

      hence thesis by A20, A26, A25;

    end;

    theorem :: ANPROJ_2:18

    x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 implies ex f, g, h, f1 st for a,b,c,d be Real st (( RealFuncAdd A) . ((( RealFuncAdd A) . ((( RealFuncAdd A) . ((( RealFuncExtMult A) . [a, f]),(( RealFuncExtMult A) . [b, g]))),(( RealFuncExtMult A) . [c, h]))),(( RealFuncExtMult A) . [d, f1]))) = ( RealFuncZero A) holds a = 0 & b = 0 & c = 0 & d = 0

    proof

      assume

       A1: x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4;

      consider f such that

       A2: (f . x1) = 1 & for z st z in A holds (z <> x1 implies (f . z) = 0 ) by Th10;

      consider f1 such that

       A3: (f1 . x4) = 1 & for z st z in A holds (z <> x4 implies (f1 . z) = 0 ) by Th10;

      consider h such that

       A4: (h . x3) = 1 & for z st z in A holds (z <> x3 implies (h . z) = 0 ) by Th10;

      consider g such that

       A5: (g . x2) = 1 & for z st z in A holds (z <> x2 implies (g . z) = 0 ) by Th10;

      take f, g, h, f1;

      let a,b,c,d be Real;

      assume (( RealFuncAdd A) . ((( RealFuncAdd A) . ((( RealFuncAdd A) . ((( RealFuncExtMult A) . [a, f]),(( RealFuncExtMult A) . [b, g]))),(( RealFuncExtMult A) . [c, h]))),(( RealFuncExtMult A) . [d, f1]))) = ( RealFuncZero A);

      hence thesis by A1, A2, A5, A4, A3, Th17;

    end;

    theorem :: ANPROJ_2:19



     Th19: A = {x1, x2, x3, x4} & x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 & (f . x1) = 1 & (for z st z in A holds (z <> x1 implies (f . z) = 0 )) & (g . x2) = 1 & (for z st z in A holds (z <> x2 implies (g . z) = 0 )) & (h . x3) = 1 & (for z st z in A holds (z <> x3 implies (h . z) = 0 )) & (f1 . x4) = 1 & (for z st z in A holds (z <> x4 implies (f1 . z) = 0 )) implies for h9 be Element of ( Funcs (A, REAL )) holds ex a,b,c,d be Real st h9 = (( RealFuncAdd A) . ((( RealFuncAdd A) . ((( RealFuncAdd A) . ((( RealFuncExtMult A) . [a, f]),(( RealFuncExtMult A) . [b, g]))),(( RealFuncExtMult A) . [c, h]))),(( RealFuncExtMult A) . [d, f1])))

    proof

      assume that

       A1: A = {x1, x2, x3, x4} and

       A2: x1 <> x2 and

       A3: x1 <> x3 and

       A4: x1 <> x4 and

       A5: x2 <> x3 and

       A6: x2 <> x4 and

       A7: x3 <> x4 and

       A8: (f . x1) = 1 and

       A9: for z st z in A holds (z <> x1 implies (f . z) = 0 ) and

       A10: (g . x2) = 1 and

       A11: for z st z in A holds (z <> x2 implies (g . z) = 0 ) and

       A12: (h . x3) = 1 and

       A13: for z st z in A holds (z <> x3 implies (h . z) = 0 ) and

       A14: (f1 . x4) = 1 and

       A15: for z st z in A holds (z <> x4 implies (f1 . z) = 0 );



       A16: (f . x4) = 0 & (g . x4) = 0 by A4, A6, A9, A11;



       A17: (f1 . x3) = 0 by A7, A15;



       A18: (f1 . x2) = 0 by A6, A15;



       A19: (f . x2) = 0 & (h . x2) = 0 by A2, A5, A9, A13;



       A20: (f1 . x1) = 0 by A4, A15;



       A21: (g . x1) = 0 & (h . x1) = 0 by A2, A3, A11, A13;



       A22: (h . x4) = 0 by A7, A13;

      let h9 be Element of ( Funcs (A, REAL ));

      take a = (h9 . x1), b = (h9 . x2), c = (h9 . x3), d = (h9 . x4);



       A23: (f . x3) = 0 & (g . x3) = 0 by A3, A5, A9, A11;

      now

        let x be Element of A;



         A24: x = x1 or x = x2 or x = x3 or x = x4 by A1, ENUMSET1:def 2;



         A25: ((( RealFuncAdd A) . ((( RealFuncAdd A) . ((( RealFuncAdd A) . ((( RealFuncExtMult A) . [a, f]),(( RealFuncExtMult A) . [b, g]))),(( RealFuncExtMult A) . [c, h]))),(( RealFuncExtMult A) . [d, f1]))) . x2) = (((( RealFuncAdd A) . ((( RealFuncAdd A) . ((( RealFuncExtMult A) . [a, f]),(( RealFuncExtMult A) . [b, g]))),(( RealFuncExtMult A) . [c, h]))) . x2) + ((( RealFuncExtMult A) . [d, f1]) . x2)) by FUNCSDOM: 1

        .= ((((( RealFuncAdd A) . ((( RealFuncExtMult A) . [a, f]),(( RealFuncExtMult A) . [b, g]))) . x2) + ((( RealFuncExtMult A) . [c, h]) . x2)) + ((( RealFuncExtMult A) . [d, f1]) . x2)) by FUNCSDOM: 1

        .= (((((( RealFuncExtMult A) . [a, f]) . x2) + ((( RealFuncExtMult A) . [b, g]) . x2)) + ((( RealFuncExtMult A) . [c, h]) . x2)) + ((( RealFuncExtMult A) . [d, f1]) . x2)) by FUNCSDOM: 1

        .= (((((( RealFuncExtMult A) . [a, f]) . x2) + ((( RealFuncExtMult A) . [b, g]) . x2)) + ((( RealFuncExtMult A) . [c, h]) . x2)) + (d * (f1 . x2))) by FUNCSDOM: 4

        .= (((((( RealFuncExtMult A) . [a, f]) . x2) + ((( RealFuncExtMult A) . [b, g]) . x2)) + (c * (h . x2))) + (d * (f1 . x2))) by FUNCSDOM: 4

        .= (((((( RealFuncExtMult A) . [a, f]) . x2) + (b * (g . x2))) + (c * (h . x2))) + (d * (f1 . x2))) by FUNCSDOM: 4

        .= ((((a * 0 ) + (b * 1)) + (c * 0 )) + (d * 0 )) by A10, A19, A18, FUNCSDOM: 4

        .= (h9 . x2);



         A26: ((( RealFuncAdd A) . ((( RealFuncAdd A) . ((( RealFuncAdd A) . ((( RealFuncExtMult A) . [a, f]),(( RealFuncExtMult A) . [b, g]))),(( RealFuncExtMult A) . [c, h]))),(( RealFuncExtMult A) . [d, f1]))) . x4) = (((( RealFuncAdd A) . ((( RealFuncAdd A) . ((( RealFuncExtMult A) . [a, f]),(( RealFuncExtMult A) . [b, g]))),(( RealFuncExtMult A) . [c, h]))) . x4) + ((( RealFuncExtMult A) . [d, f1]) . x4)) by FUNCSDOM: 1

        .= ((((( RealFuncAdd A) . ((( RealFuncExtMult A) . [a, f]),(( RealFuncExtMult A) . [b, g]))) . x4) + ((( RealFuncExtMult A) . [c, h]) . x4)) + ((( RealFuncExtMult A) . [d, f1]) . x4)) by FUNCSDOM: 1

        .= (((((( RealFuncExtMult A) . [a, f]) . x4) + ((( RealFuncExtMult A) . [b, g]) . x4)) + ((( RealFuncExtMult A) . [c, h]) . x4)) + ((( RealFuncExtMult A) . [d, f1]) . x4)) by FUNCSDOM: 1

        .= (((((( RealFuncExtMult A) . [a, f]) . x4) + ((( RealFuncExtMult A) . [b, g]) . x4)) + ((( RealFuncExtMult A) . [c, h]) . x4)) + (d * (f1 . x4))) by FUNCSDOM: 4

        .= (((((( RealFuncExtMult A) . [a, f]) . x4) + ((( RealFuncExtMult A) . [b, g]) . x4)) + (c * (h . x4))) + (d * (f1 . x4))) by FUNCSDOM: 4

        .= (((((( RealFuncExtMult A) . [a, f]) . x4) + (b * (g . x4))) + (c * (h . x4))) + (d * (f1 . x4))) by FUNCSDOM: 4

        .= ((((a * 0 ) + (b * 0 )) + (c * 0 )) + (d * 1)) by A14, A16, A22, FUNCSDOM: 4

        .= (h9 . x4);



         A27: ((( RealFuncAdd A) . ((( RealFuncAdd A) . ((( RealFuncAdd A) . ((( RealFuncExtMult A) . [a, f]),(( RealFuncExtMult A) . [b, g]))),(( RealFuncExtMult A) . [c, h]))),(( RealFuncExtMult A) . [d, f1]))) . x3) = (((( RealFuncAdd A) . ((( RealFuncAdd A) . ((( RealFuncExtMult A) . [a, f]),(( RealFuncExtMult A) . [b, g]))),(( RealFuncExtMult A) . [c, h]))) . x3) + ((( RealFuncExtMult A) . [d, f1]) . x3)) by FUNCSDOM: 1

        .= ((((( RealFuncAdd A) . ((( RealFuncExtMult A) . [a, f]),(( RealFuncExtMult A) . [b, g]))) . x3) + ((( RealFuncExtMult A) . [c, h]) . x3)) + ((( RealFuncExtMult A) . [d, f1]) . x3)) by FUNCSDOM: 1

        .= (((((( RealFuncExtMult A) . [a, f]) . x3) + ((( RealFuncExtMult A) . [b, g]) . x3)) + ((( RealFuncExtMult A) . [c, h]) . x3)) + ((( RealFuncExtMult A) . [d, f1]) . x3)) by FUNCSDOM: 1

        .= (((((( RealFuncExtMult A) . [a, f]) . x3) + ((( RealFuncExtMult A) . [b, g]) . x3)) + ((( RealFuncExtMult A) . [c, h]) . x3)) + (d * (f1 . x3))) by FUNCSDOM: 4

        .= (((((( RealFuncExtMult A) . [a, f]) . x3) + ((( RealFuncExtMult A) . [b, g]) . x3)) + (c * (h . x3))) + (d * (f1 . x3))) by FUNCSDOM: 4

        .= (((((( RealFuncExtMult A) . [a, f]) . x3) + (b * (g . x3))) + (c * (h . x3))) + (d * (f1 . x3))) by FUNCSDOM: 4

        .= ((((a * 0 ) + (b * 0 )) + (c * 1)) + (d * 0 )) by A12, A23, A17, FUNCSDOM: 4

        .= (h9 . x3);

        ((( RealFuncAdd A) . ((( RealFuncAdd A) . ((( RealFuncAdd A) . ((( RealFuncExtMult A) . [a, f]),(( RealFuncExtMult A) . [b, g]))),(( RealFuncExtMult A) . [c, h]))),(( RealFuncExtMult A) . [d, f1]))) . x1) = (((( RealFuncAdd A) . ((( RealFuncAdd A) . ((( RealFuncExtMult A) . [a, f]),(( RealFuncExtMult A) . [b, g]))),(( RealFuncExtMult A) . [c, h]))) . x1) + ((( RealFuncExtMult A) . [d, f1]) . x1)) by FUNCSDOM: 1

        .= ((((( RealFuncAdd A) . ((( RealFuncExtMult A) . [a, f]),(( RealFuncExtMult A) . [b, g]))) . x1) + ((( RealFuncExtMult A) . [c, h]) . x1)) + ((( RealFuncExtMult A) . [d, f1]) . x1)) by FUNCSDOM: 1

        .= (((((( RealFuncExtMult A) . [a, f]) . x1) + ((( RealFuncExtMult A) . [b, g]) . x1)) + ((( RealFuncExtMult A) . [c, h]) . x1)) + ((( RealFuncExtMult A) . [d, f1]) . x1)) by FUNCSDOM: 1

        .= (((((( RealFuncExtMult A) . [a, f]) . x1) + ((( RealFuncExtMult A) . [b, g]) . x1)) + ((( RealFuncExtMult A) . [c, h]) . x1)) + (d * (f1 . x1))) by FUNCSDOM: 4

        .= (((((( RealFuncExtMult A) . [a, f]) . x1) + ((( RealFuncExtMult A) . [b, g]) . x1)) + (c * (h . x1))) + (d * (f1 . x1))) by FUNCSDOM: 4

        .= (((((( RealFuncExtMult A) . [a, f]) . x1) + (b * (g . x1))) + (c * (h . x1))) + (d * (f1 . x1))) by FUNCSDOM: 4

        .= ((((a * 1) + (b * 0 )) + (c * 0 )) + (d * 0 )) by A8, A21, A20, FUNCSDOM: 4

        .= (h9 . x1);

        hence (h9 . x) = ((( RealFuncAdd A) . ((( RealFuncAdd A) . ((( RealFuncAdd A) . ((( RealFuncExtMult A) . [a, f]),(( RealFuncExtMult A) . [b, g]))),(( RealFuncExtMult A) . [c, h]))),(( RealFuncExtMult A) . [d, f1]))) . x) by A24, A25, A27, A26;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: ANPROJ_2:20

    A = {x1, x2, x3, x4} & x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 implies ex f, g, h, f1 st for h9 be Element of ( Funcs (A, REAL )) holds ex a,b,c,d be Real st h9 = (( RealFuncAdd A) . ((( RealFuncAdd A) . ((( RealFuncAdd A) . ((( RealFuncExtMult A) . [a, f]),(( RealFuncExtMult A) . [b, g]))),(( RealFuncExtMult A) . [c, h]))),(( RealFuncExtMult A) . [d, f1])))

    proof

      assume

       A1: A = {x1, x2, x3, x4} & x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4;

      consider f such that

       A2: (f . x1) = 1 & for z st z in A holds (z <> x1 implies (f . z) = 0 ) by Th10;

      consider f1 such that

       A3: (f1 . x4) = 1 & for z st z in A holds (z <> x4 implies (f1 . z) = 0 ) by Th10;

      consider h such that

       A4: (h . x3) = 1 & for z st z in A holds (z <> x3 implies (h . z) = 0 ) by Th10;

      consider g such that

       A5: (g . x2) = 1 & for z st z in A holds (z <> x2 implies (g . z) = 0 ) by Th10;

      take f, g, h, f1;

      let h9 be Element of ( Funcs (A, REAL ));

      thus thesis by A1, A2, A5, A4, A3, Th19;

    end;

    theorem :: ANPROJ_2:21



     Th21: A = {x1, x2, x3, x4} & x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 implies ex f, g, h, f1 st (for a,b,c,d be Real st (( RealFuncAdd A) . ((( RealFuncAdd A) . ((( RealFuncAdd A) . ((( RealFuncExtMult A) . [a, f]),(( RealFuncExtMult A) . [b, g]))),(( RealFuncExtMult A) . [c, h]))),(( RealFuncExtMult A) . [d, f1]))) = ( RealFuncZero A) holds a = 0 & b = 0 & c = 0 & d = 0 ) & for h9 be Element of ( Funcs (A, REAL )) holds ex a,b,c,d be Real st h9 = (( RealFuncAdd A) . ((( RealFuncAdd A) . ((( RealFuncAdd A) . ((( RealFuncExtMult A) . [a, f]),(( RealFuncExtMult A) . [b, g]))),(( RealFuncExtMult A) . [c, h]))),(( RealFuncExtMult A) . [d, f1])))

    proof

      assume

       A1: A = {x1, x2, x3, x4} & x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4;

      consider f such that

       A2: (f . x1) = 1 & for z st z in A holds (z <> x1 implies (f . z) = 0 ) by Th10;

      consider f1 such that

       A3: (f1 . x4) = 1 & for z st z in A holds (z <> x4 implies (f1 . z) = 0 ) by Th10;

      consider h such that

       A4: (h . x3) = 1 & for z st z in A holds (z <> x3 implies (h . z) = 0 ) by Th10;

      consider g such that

       A5: (g . x2) = 1 & for z st z in A holds (z <> x2 implies (g . z) = 0 ) by Th10;

      take f, g, h, f1;

      thus thesis by A1, A2, A5, A4, A3, Th17, Th19;

    end;



     Lm31: ex A, x1, x2, x3, x4 st A = {x1, x2, x3, x4} & x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4

    proof

      reconsider A = { 0 , 1, 2, 3} as non empty set;

      take A;

      reconsider x1 = 0 , x2 = 1, x3 = 2, x4 = 3 as Element of A by ENUMSET1:def 2;

      take x1, x2, x3, x4;

      thus thesis;

    end;

    theorem :: ANPROJ_2:22



     Th22: ex V be non trivial RealLinearSpace st ex u,v,w,u1 be Element of V st (for a, b, c, d st ((((a * u) + (b * v)) + (c * w)) + (d * u1)) = ( 0. V) holds a = 0 & b = 0 & c = 0 & d = 0 ) & for y be Element of V holds ex a, b, c, d st y = ((((a * u) + (b * v)) + (c * w)) + (d * u1))

    proof

      consider A, x1, x2, x3, x4 such that

       A1: A = {x1, x2, x3, x4} & x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 by Lm31;

      set V = ( RealVectSpace A);

      consider f, g, h, f1 such that

       A2: for a,b,c,d be Real st (( RealFuncAdd A) . ((( RealFuncAdd A) . ((( RealFuncAdd A) . ((( RealFuncExtMult A) . [a, f]),(( RealFuncExtMult A) . [b, g]))),(( RealFuncExtMult A) . [c, h]))),(( RealFuncExtMult A) . [d, f1]))) = ( RealFuncZero A) holds a = 0 & b = 0 & c = 0 & d = 0 and

       A3: for h9 be Element of ( Funcs (A, REAL )) holds ex a,b,c,d be Real st h9 = (( RealFuncAdd A) . ((( RealFuncAdd A) . ((( RealFuncAdd A) . ((( RealFuncExtMult A) . [a, f]),(( RealFuncExtMult A) . [b, g]))),(( RealFuncExtMult A) . [c, h]))),(( RealFuncExtMult A) . [d, f1]))) by A1, Th21;

      reconsider u = f, v = g, w = h, u1 = f1 as Element of V;

      for a, b, c, d st ((((a * u) + (b * v)) + (c * w)) + (d * u1)) = ( 0. V) holds a = 0 & b = 0 & c = 0 & d = 0 by A2;

      then not u is zero by Th2;

      then

       A4: u <> ( 0. V);



       A5: for y be Element of V holds ex a, b, c, d st y = ((((a * u) + (b * v)) + (c * w)) + (d * u1))

      proof

        let y be Element of V;

        reconsider h9 = y as Element of ( Funcs (A, REAL ));

        consider a,b,c,d be Real such that

         A6: h9 = (( RealFuncAdd A) . ((( RealFuncAdd A) . ((( RealFuncAdd A) . ((( RealFuncExtMult A) . [a, f]),(( RealFuncExtMult A) . [b, g]))),(( RealFuncExtMult A) . [c, h]))),(( RealFuncExtMult A) . [d, f1]))) by A3;

        h9 = ((((a * u) + (b * v)) + (c * w)) + (d * u1)) by A6;

        hence thesis;

      end;

      reconsider V as non trivial RealLinearSpace by A4, STRUCT_0:def 18;

      take V;

      reconsider u, v, w, u1 as Element of V;

      take u, v, w, u1;

      thus for a, b, c, d st ((((a * u) + (b * v)) + (c * w)) + (d * u1)) = ( 0. V) holds a = 0 & b = 0 & c = 0 & d = 0 by A2;

      let y be Element of V;

      ex a, b, c, d st y = ((((a * u) + (b * v)) + (c * w)) + (d * u1)) by A5;

      hence thesis;

    end;

    definition

      let IT be RealLinearSpace;

      :: ANPROJ_2:def6

      attr IT is up-3-dimensional means

      : Def6: ex u,v,w1 be Element of IT st for a, b, c st (((a * u) + (b * v)) + (c * w1)) = ( 0. IT) holds a = 0 & b = 0 & c = 0 ;

    end

    registration

      cluster up-3-dimensional for RealLinearSpace;

      existence by Th16, Def6;

    end

    registration

      cluster up-3-dimensional -> non trivial for RealLinearSpace;

      coherence

      proof

        let V be RealLinearSpace;

        given u,v,w1 be Element of V such that

         A1: for a, b, c st (((a * u) + (b * v)) + (c * w1)) = ( 0. V) holds a = 0 & b = 0 & c = 0 ;

        now

          assume w1 = ( 0. V);

          then

           A2: ( 0. V) = (1 * w1) by RLVECT_1: 10;

          ( 0. V) = ( 0 * u) & ( 0. V) = ( 0 * v) by RLVECT_1: 10;



          then ( 0. V) = (( 0 * u) + ( 0 * v)) by RLVECT_1: 4

          .= ((( 0 * u) + ( 0 * v)) + (1 * w1)) by A2, RLVECT_1: 4;

          hence contradiction by A1;

        end;

        hence thesis;

      end;

    end

    definition

      let CS be non empty CollStr;

      :: original: reflexive

      redefine

      :: ANPROJ_2:def7

      attr CS is reflexive means

      : Def7: for p,q,r be Element of CS holds (p,q,p) are_collinear & (p,p,q) are_collinear & (p,q,q) are_collinear ;

      compatibility

      proof

        thus CS is reflexive implies for p,q,r be Element of CS holds (p,q,p) are_collinear & (p,p,q) are_collinear & (p,q,q) are_collinear ;

        assume

         A1: for p,q,r be Element of CS holds (p,q,p) are_collinear & (p,p,q) are_collinear & (p,q,q) are_collinear ;

        let p,q,r be Element of CS such that

         A2: p = q or p = r or q = r;

        per cases by A2;

          suppose p = q;

          then (p,q,r) are_collinear by A1;

          hence thesis;

        end;

          suppose p = r;

          then (p,q,r) are_collinear by A1;

          hence thesis;

        end;

          suppose q = r;

          then (p,q,r) are_collinear by A1;

          hence thesis;

        end;

      end;

      :: original: transitive

      redefine

      :: ANPROJ_2:def8

      attr CS is transitive means

      : Def8: for p,q,r,r1,r2 be Element of CS st p <> q & (p,q,r) are_collinear & (p,q,r1) are_collinear & (p,q,r2) are_collinear holds (r,r1,r2) are_collinear ;

      compatibility

      proof

        thus CS is transitive implies for p,q,r,r1,r2 be Element of CS st p <> q & (p,q,r) are_collinear & (p,q,r1) are_collinear & (p,q,r2) are_collinear holds (r,r1,r2) are_collinear ;

        assume

         A3: for p,q,r,r1,r2 be Element of CS st p <> q & (p,q,r) are_collinear & (p,q,r1) are_collinear & (p,q,r2) are_collinear holds (r,r1,r2) are_collinear ;

        let p,q,r,r1,r2 be Element of CS such that

         A4: p <> q and

         A5: [p, q, r] in the Collinearity of CS & [p, q, r1] in the Collinearity of CS and

         A6: [p, q, r2] in the Collinearity of CS;



         A7: (p,q,r2) are_collinear by A6;

        (p,q,r) are_collinear & (p,q,r1) are_collinear by A5;

        then (r,r1,r2) are_collinear by A3, A4, A7;

        hence thesis;

      end;

    end

    definition

      let IT be non empty CollStr;

      :: ANPROJ_2:def9

      attr IT is Vebleian means

      : Def9: for p,p1,p2,r,r1 be Element of IT st (p,p1,r) are_collinear & (p1,p2,r1) are_collinear holds ex r2 be Element of IT st (p,p2,r2) are_collinear & (r,r1,r2) are_collinear ;

      :: ANPROJ_2:def10

      attr IT is at_least_3rank means

      : Def10: for p,q be Element of IT holds ex r be Element of IT st p <> r & q <> r & (p,q,r) are_collinear ;

    end

    reserve V for non trivial RealLinearSpace;

    reserve u,v,w,y,u1,v1,w1,u2,w2 for Element of V;

    reserve p,p1,p2,p3,q,q1,q2,q3,r,r1,r2,r3 for Element of ( ProjectiveSpace V);

    theorem :: ANPROJ_2:23



     Th23: (p,q,r) are_collinear iff ex u, v, w st p = ( Dir u) & q = ( Dir v) & r = ( Dir w) & not u is zero & not v is zero & not w is zero & (u,v,w) are_LinDep by ANPROJ_1: 24, ANPROJ_1: 25;



     Lm32: ( ProjectiveSpace V) is reflexive

    proof

      let p, q;

      consider u such that

       A1: not u is zero & p = ( Dir u) by ANPROJ_1: 26;

      consider v such that

       A2: not v is zero & q = ( Dir v) by ANPROJ_1: 26;



       A3: (u,v,v) are_LinDep by ANPROJ_1: 11;

      (u,v,u) are_LinDep & (u,u,v) are_LinDep by ANPROJ_1: 11;

      hence thesis by A1, A2, A3, Th23;

    end;



     Lm33: ( ProjectiveSpace V) is transitive

    proof

      let p, q, r, r1, r2;

      assume that

       A1: p <> q and

       A2: (p,q,r) are_collinear and

       A3: (p,q,r1) are_collinear and

       A4: (p,q,r2) are_collinear ;

      consider u1, v1, w1 such that

       A5: p = ( Dir u1) and

       A6: q = ( Dir v1) and

       A7: r = ( Dir w1) and

       A8: not u1 is zero and

       A9: not v1 is zero and

       A10: not w1 is zero and

       A11: (u1,v1,w1) are_LinDep by A2, Th23;

      consider v such that

       A12: not v is zero and

       A13: q = ( Dir v) by ANPROJ_1: 26;



       A14: are_Prop (v1,v) by A12, A13, A6, A9, ANPROJ_1: 22;

      consider u3,v3,w3 be Element of V such that

       A15: p = ( Dir u3) and

       A16: q = ( Dir v3) and

       A17: r2 = ( Dir w3) and

       A18: not u3 is zero and

       A19: not v3 is zero and

       A20: not w3 is zero and

       A21: (u3,v3,w3) are_LinDep by A4, Th23;



       A22: are_Prop (v3,v) by A12, A13, A16, A19, ANPROJ_1: 22;

      consider u2,v2,w2 be Element of V such that

       A23: p = ( Dir u2) and

       A24: q = ( Dir v2) and

       A25: r1 = ( Dir w2) and

       A26: not u2 is zero and

       A27: not v2 is zero and

       A28: not w2 is zero and

       A29: (u2,v2,w2) are_LinDep by A3, Th23;



       A30: are_Prop (v2,v) by A12, A13, A24, A27, ANPROJ_1: 22;

      consider u such that

       A31: not u is zero and

       A32: p = ( Dir u) by ANPROJ_1: 26;

       are_Prop (u1,u) by A31, A32, A5, A8, ANPROJ_1: 22;

      then

       A33: (u,v,w1) are_LinDep by A11, A14, ANPROJ_1: 4;

       are_Prop (u3,u) by A31, A32, A15, A18, ANPROJ_1: 22;

      then

       A34: (u,v,w3) are_LinDep by A21, A22, ANPROJ_1: 4;

       are_Prop (u2,u) by A31, A32, A23, A26, ANPROJ_1: 22;

      then

       A35: (u,v,w2) are_LinDep by A29, A30, ANPROJ_1: 4;

       not are_Prop (u,v) by A1, A31, A32, A12, A13, ANPROJ_1: 22;

      then (w1,w2,w3) are_LinDep by A31, A12, A33, A35, A34, ANPROJ_1: 14;

      hence thesis by A7, A10, A25, A28, A17, A20, Th23;

    end;

    registration

      let V;

      cluster ( ProjectiveSpace V) -> reflexive transitive;

      coherence by Lm32, Lm33;

    end

    theorem :: ANPROJ_2:24



     Th24: (p,q,r) are_collinear implies (p,r,q) are_collinear & (q,p,r) are_collinear & (r,q,p) are_collinear & (r,p,q) are_collinear & (q,r,p) are_collinear

    proof

      assume (p,q,r) are_collinear ;

      then

      consider u, v, w such that

       A1: p = ( Dir u) & q = ( Dir v) & r = ( Dir w) & not u is zero & not v is zero & not w is zero and

       A2: (u,v,w) are_LinDep by Th23;



       A3: (w,v,u) are_LinDep & (w,u,v) are_LinDep by A2, ANPROJ_1: 5;



       A4: (v,w,u) are_LinDep by A2, ANPROJ_1: 5;

      (u,w,v) are_LinDep & (v,u,w) are_LinDep by A2, ANPROJ_1: 5;

      hence thesis by A1, A3, A4, Th23;

    end;



     Lm34: (p,p1,p2) are_collinear & (p,p1,r) are_collinear & (p1,p2,r1) are_collinear implies ex r2 st (p,p2,r2) are_collinear & (r,r1,r2) are_collinear

    proof

      assume that

       A1: (p,p1,p2) are_collinear and

       A2: (p,p1,r) are_collinear and

       A3: (p1,p2,r1) are_collinear ;

       A4:

      now

         A5:

        now

          assume

           A6: p1 <> p;

          take r;



           A7: (r,r1,r) are_collinear by Def7;

          (p,p1,p) are_collinear by Def7;

          then (p,p2,r) are_collinear by A1, A2, A6, Def8;

          hence thesis by A7;

        end;

         A8:

        now

          assume

           A9: p1 <> p2;

          take r1;



           A10: (r,r1,r1) are_collinear by Def7;

          (p1,p2,p) are_collinear & (p1,p2,p2) are_collinear by A1, Def7, Th24;

          then (p,p2,r1) are_collinear by A3, A9, Def8;

          hence thesis by A10;

        end;

        assume p <> p2;

        hence thesis by A5, A8;

      end;

      now

        assume p = p2;

        then

         A11: (p,p2,r) are_collinear by Def7;

        take r;

        (r,r1,r) are_collinear by Def7;

        hence thesis by A11;

      end;

      hence thesis by A4;

    end;



     Lm35: not (p,p1,p2) are_collinear & (p,p1,r) are_collinear & (p1,p2,r1) are_collinear implies ex r2 st (p,p2,r2) are_collinear & (r,r1,r2) are_collinear

    proof

      assume that

       A1: not (p,p1,p2) are_collinear and

       A2: (p,p1,r) are_collinear and

       A3: (p1,p2,r1) are_collinear ;

      consider u,v,t be Element of V such that

       A4: p = ( Dir u) and

       A5: p1 = ( Dir v) and

       A6: r = ( Dir t) and

       A7: not u is zero and

       A8: not v is zero and

       A9: not t is zero and

       A10: (u,v,t) are_LinDep by A2, Th23;

      consider v1,w,s be Element of V such that

       A11: p1 = ( Dir v1) and

       A12: p2 = ( Dir w) and

       A13: r1 = ( Dir s) and

       A14: not v1 is zero and

       A15: not w is zero and

       A16: not s is zero and

       A17: (v1,w,s) are_LinDep by A3, Th23;

       are_Prop (v1,v) by A5, A8, A11, A14, ANPROJ_1: 22;

      then

       A18: (v,w,s) are_LinDep by A17, ANPROJ_1: 4;

       not (u,v,w) are_LinDep by A1, A4, A5, A7, A8, A12, A15, Th23;

      then

      consider y such that

       A19: (u,w,y) are_LinDep & (t,s,y) are_LinDep and

       A20: not y is zero by A10, A18, ANPROJ_1: 15;

      reconsider r2 = ( Dir y) as Element of ( ProjectiveSpace V) by A20, ANPROJ_1: 26;

      take r2;

      thus thesis by A4, A6, A7, A9, A12, A13, A15, A16, A19, A20, Th23;

    end;



     Lm36: ( ProjectiveSpace V) is Vebleian

    proof

      let p, p1, p2, r, r1;

      assume

       A1: (p,p1,r) are_collinear & (p1,p2,r1) are_collinear ;

      then (p,p1,p2) are_collinear implies thesis by Lm34;

      hence thesis by A1, Lm35;

    end;

    registration

      let V;

      cluster ( ProjectiveSpace V) -> Vebleian;

      coherence by Lm36;

    end



     Lm37: V is up-3-dimensional implies ( ProjectiveSpace V) is proper

    proof

      given u, v, w such that

       A1: for a, b, c st (((a * u) + (b * v)) + (c * w)) = ( 0. V) holds a = 0 & b = 0 & c = 0 ;



       A2: not (u,v,w) are_LinDep by A1;



       A3: not w is zero by A1, Th1;



       A4: not u is zero & not v is zero by A1, Th1;

      then

      reconsider p = ( Dir u), q = ( Dir v), r = ( Dir w) as Element of ( ProjectiveSpace V) by A3, ANPROJ_1: 26;

      take p, q, r;

      assume (p,q,r) are_collinear ;

      then [( Dir u), ( Dir v), ( Dir w)] in the Collinearity of ( ProjectiveSpace V);

      hence contradiction by A4, A3, A2, ANPROJ_1: 25;

    end;

    registration

      let V be up-3-dimensional RealLinearSpace;

      cluster ( ProjectiveSpace V) -> proper;

      coherence by Lm37;

    end

    theorem :: ANPROJ_2:25



     Th25: (ex u, v st for a, b st ((a * u) + (b * v)) = ( 0. V) holds a = 0 & b = 0 ) implies ( ProjectiveSpace V) is at_least_3rank

    proof

      given u, v such that

       A1: for a, b st ((a * u) + (b * v)) = ( 0. V) holds a = 0 & b = 0 ;



       A2: not are_Prop (u,v) by A1, Lm1;

      let p, q;

      consider y such that

       A3: not y is zero & p = ( Dir y) by ANPROJ_1: 26;

      consider w such that

       A4: not w is zero & q = ( Dir w) by ANPROJ_1: 26;

       not u is zero & not v is zero by A1, Lm1;

      then

      consider z be Element of V such that

       A5: not z is zero and

       A6: (y,w,z) are_LinDep and

       A7: not are_Prop (y,z) and

       A8: not are_Prop (w,z) by A2, ANPROJ_1: 16;

      reconsider r = ( Dir z) as Element of ( ProjectiveSpace V) by A5, ANPROJ_1: 26;

      take r;

      thus p <> r by A3, A5, A7, ANPROJ_1: 22;

      thus q <> r by A4, A5, A8, ANPROJ_1: 22;

      thus thesis by A3, A4, A5, A6, Th23;

    end;



     Lm38: V is up-3-dimensional implies ( ProjectiveSpace V) is at_least_3rank

    proof

      given u, v, w1 such that

       A1: for a, b, c st (((a * u) + (b * v)) + (c * w1)) = ( 0. V) holds a = 0 & b = 0 & c = 0 ;

      now

        let a, b;

        assume ((a * u) + (b * v)) = ( 0. V);



        then ( 0. V) = (((a * u) + (b * v)) + ( 0. V)) by RLVECT_1: 4

        .= (((a * u) + (b * v)) + ( 0 * w1)) by RLVECT_1: 10;

        hence a = 0 & b = 0 by A1;

      end;

      hence thesis by Th25;

    end;

    registration

      let V be up-3-dimensional RealLinearSpace;

      cluster ( ProjectiveSpace V) -> at_least_3rank;

      coherence by Lm38;

    end

    registration

      cluster transitive reflexive proper Vebleian at_least_3rank for non empty CollStr;

      existence

      proof

        set V0 = the up-3-dimensional RealLinearSpace;

        take ( ProjectiveSpace V0);

        thus thesis;

      end;

    end

    definition

      mode CollProjectiveSpace is reflexive transitive Vebleian at_least_3rank proper non empty CollStr;

    end

    definition

      let IT be non empty CollStr;

      :: ANPROJ_2:def11

      attr IT is Fanoian means for p1,r2,q,r1,q1,p,r be Element of IT holds ((p1,r2,q) are_collinear & (r1,q1,q) are_collinear & (p1,r1,p) are_collinear & (r2,q1,p) are_collinear & (p1,q1,r) are_collinear & (r2,r1,r) are_collinear & (p,q,r) are_collinear implies ((p1,r2,q1) are_collinear or (p1,r2,r1) are_collinear or (p1,r1,q1) are_collinear or (r2,r1,q1) are_collinear ));

      :: ANPROJ_2:def12

      attr IT is Desarguesian means for o,p1,p2,p3,q1,q2,q3,r1,r2,r3 be Element of IT st o <> q1 & p1 <> q1 & o <> q2 & p2 <> q2 & o <> q3 & p3 <> q3 & not (o,p1,p2) are_collinear & not (o,p1,p3) are_collinear & not (o,p2,p3) are_collinear & (p1,p2,r3) are_collinear & (q1,q2,r3) are_collinear & (p2,p3,r1) are_collinear & (q2,q3,r1) are_collinear & (p1,p3,r2) are_collinear & (q1,q3,r2) are_collinear & (o,p1,q1) are_collinear & (o,p2,q2) are_collinear & (o,p3,q3) are_collinear holds (r1,r2,r3) are_collinear ;

      :: ANPROJ_2:def13

      attr IT is Pappian means for o,p1,p2,p3,q1,q2,q3,r1,r2,r3 be Element of IT st o <> p2 & o <> p3 & p2 <> p3 & p1 <> p2 & p1 <> p3 & o <> q2 & o <> q3 & q2 <> q3 & q1 <> q2 & q1 <> q3 & not (o,p1,q1) are_collinear & (o,p1,p2) are_collinear & (o,p1,p3) are_collinear & (o,q1,q2) are_collinear & (o,q1,q3) are_collinear & (p1,q2,r3) are_collinear & (q1,p2,r3) are_collinear & (p1,q3,r2) are_collinear & (p3,q1,r2) are_collinear & (p2,q3,r1) are_collinear & (p3,q2,r1) are_collinear holds (r1,r2,r3) are_collinear ;

    end

    definition

      let IT be CollProjectiveSpace;

      :: ANPROJ_2:def14

      attr IT is 2-dimensional means

      : Def14: for p,p1,q,q1 be Element of IT holds ex r be Element of IT st (p,p1,r) are_collinear & (q,q1,r) are_collinear ;

    end

    notation

      let IT be CollProjectiveSpace;

      antonym IT is up-3-dimensional for IT is 2-dimensional;

    end

    definition

      let IT be CollProjectiveSpace;

      :: ANPROJ_2:def15

      attr IT is at_most-3-dimensional means for p,p1,q,q1,r2 be Element of IT holds ex r,r1 be Element of IT st (p,q,r) are_collinear & (p1,q1,r1) are_collinear & (r2,r,r1) are_collinear ;

    end

    theorem :: ANPROJ_2:26



     Th26: (p1,r2,q) are_collinear & (r1,q1,q) are_collinear & (p1,r1,p) are_collinear & (r2,q1,p) are_collinear & (p1,q1,r) are_collinear & (r2,r1,r) are_collinear & (p,q,r) are_collinear implies ((p1,r2,q1) are_collinear or (p1,r2,r1) are_collinear or (p1,r1,q1) are_collinear or (r2,r1,q1) are_collinear )

    proof

      assume that

       A1: (p1,r2,q) are_collinear and

       A2: (r1,q1,q) are_collinear and

       A3: (p1,r1,p) are_collinear and

       A4: (r2,q1,p) are_collinear and

       A5: (p1,q1,r) are_collinear and

       A6: (r2,r1,r) are_collinear and

       A7: (p,q,r) are_collinear ;

      consider u1,w1,x be Element of V such that

       A8: p1 = ( Dir u1) and

       A9: r1 = ( Dir w1) and

       A10: p = ( Dir x) and

       A11: not u1 is zero and

       A12: not w1 is zero and

       A13: not x is zero and

       A14: (u1,w1,x) are_LinDep by A3, Th23;

      consider u,v,z be Element of V such that

       A15: p1 = ( Dir u) and

       A16: r2 = ( Dir v) and

       A17: q = ( Dir z) and

       A18: not u is zero and

       A19: not v is zero and

       A20: not z is zero and

       A21: (u,v,z) are_LinDep by A1, Th23;

      consider w,y,z1 be Element of V such that

       A22: r1 = ( Dir w) and

       A23: q1 = ( Dir y) and

       A24: q = ( Dir z1) and

       A25: not w is zero and

       A26: not y is zero and

       A27: not z1 is zero and

       A28: (w,y,z1) are_LinDep by A2, Th23;



       A29: are_Prop (w1,w) by A22, A25, A9, A12, ANPROJ_1: 22;

       are_Prop (z1,z) by A17, A20, A24, A27, ANPROJ_1: 22;

      then

       A30: (w,y,z) are_LinDep by A28, ANPROJ_1: 4;

      consider x2,z2,t2 be Element of V such that

       A31: p = ( Dir x2) and

       A32: q = ( Dir z2) and

       A33: r = ( Dir t2) and

       A34: not x2 is zero and

       A35: not z2 is zero and

       A36: not t2 is zero and

       A37: (x2,z2,t2) are_LinDep by A7, Th23;



       A38: are_Prop (x2,x) by A10, A13, A31, A34, ANPROJ_1: 22;

      consider u2,y2,t be Element of V such that

       A39: p1 = ( Dir u2) and

       A40: q1 = ( Dir y2) and

       A41: r = ( Dir t) and

       A42: not u2 is zero and

       A43: not y2 is zero and

       A44: not t is zero and

       A45: (u2,y2,t) are_LinDep by A5, Th23;



       A46: are_Prop (y2,y) by A23, A26, A40, A43, ANPROJ_1: 22;



       A47: are_Prop (t2,t) by A41, A44, A33, A36, ANPROJ_1: 22;

       are_Prop (z2,z) by A17, A20, A32, A35, ANPROJ_1: 22;

      then

       A48: (x,z,t) are_LinDep by A37, A38, A47, ANPROJ_1: 4;

       are_Prop (u2,u) by A15, A18, A39, A42, ANPROJ_1: 22;

      then

       A49: (u,y,t) are_LinDep by A45, A46, ANPROJ_1: 4;

      consider v2,w2,t1 be Element of V such that

       A50: r2 = ( Dir v2) and

       A51: r1 = ( Dir w2) and

       A52: r = ( Dir t1) and

       A53: not v2 is zero and

       A54: not w2 is zero and

       A55: not t1 is zero and

       A56: (v2,w2,t1) are_LinDep by A6, Th23;



       A57: are_Prop (t1,t) by A41, A44, A52, A55, ANPROJ_1: 22;

       are_Prop (u1,u) by A15, A18, A8, A11, ANPROJ_1: 22;

      then

       A58: (u,w,x) are_LinDep by A14, A29, ANPROJ_1: 4;

      consider v1,y1,x1 be Element of V such that

       A59: r2 = ( Dir v1) and

       A60: q1 = ( Dir y1) and

       A61: p = ( Dir x1) and

       A62: not v1 is zero and

       A63: not y1 is zero and

       A64: not x1 is zero and

       A65: (v1,y1,x1) are_LinDep by A4, Th23;



       A66: are_Prop (x1,x) by A10, A13, A61, A64, ANPROJ_1: 22;



       A67: are_Prop (w2,w) by A22, A25, A51, A54, ANPROJ_1: 22;

       are_Prop (v2,v) by A16, A19, A50, A53, ANPROJ_1: 22;

      then

       A68: (v,w,t) are_LinDep by A56, A67, A57, ANPROJ_1: 4;



       A69: are_Prop (y1,y) by A23, A26, A60, A63, ANPROJ_1: 22;

       are_Prop (v1,v) by A16, A19, A59, A62, ANPROJ_1: 22;

      then (v,y,x) are_LinDep by A65, A69, A66, ANPROJ_1: 4;

      then (u,v,y) are_LinDep or (u,v,w) are_LinDep or (u,w,y) are_LinDep or (v,w,y) are_LinDep by A20, A21, A13, A44, A30, A58, A49, A68, A48, ANPROJ_1: 18;

      hence thesis by A15, A16, A18, A19, A22, A23, A25, A26, Th23;

    end;



     Lm39: for V be up-3-dimensional RealLinearSpace holds ( ProjectiveSpace V) is Fanoian by Th26;



     Lm40: for V be up-3-dimensional RealLinearSpace holds ( ProjectiveSpace V) is Desarguesian

    proof

      let V be up-3-dimensional RealLinearSpace;

      let o,p1,p2,p3,q1,q2,q3,r1,r2,r3 be Element of ( ProjectiveSpace V);

      assume that

       A1: o <> q1 and

       A2: p1 <> q1 and

       A3: o <> q2 and

       A4: p2 <> q2 and

       A5: o <> q3 and

       A6: p3 <> q3 and

       A7: not (o,p1,p2) are_collinear and

       A8: ( not (o,p1,p3) are_collinear ) & not (o,p2,p3) are_collinear and

       A9: (p1,p2,r3) are_collinear and

       A10: (q1,q2,r3) are_collinear and

       A11: (p2,p3,r1) are_collinear and

       A12: (q2,q3,r1) are_collinear and

       A13: (p1,p3,r2) are_collinear and

       A14: (q1,q3,r2) are_collinear and

       A15: (o,p1,q1) are_collinear and

       A16: (o,p2,q2) are_collinear and

       A17: (o,p3,q3) are_collinear ;

      consider q19,q29,r399 be Element of V such that

       A18: q1 = ( Dir q19) and

       A19: q2 = ( Dir q29) and

       A20: r3 = ( Dir r399) and

       A21: not q19 is zero and

       A22: not q29 is zero and

       A23: not r399 is zero and

       A24: (q19,q29,r399) are_LinDep by A10, Th23;

      consider q299,q39,r199 be Element of V such that

       A25: q2 = ( Dir q299) and

       A26: q3 = ( Dir q39) and

       A27: r1 = ( Dir r199) and

       A28: not q299 is zero and

       A29: not q39 is zero and

       A30: not r199 is zero and

       A31: (q299,q39,r199) are_LinDep by A12, Th23;



       A32: are_Prop (q299,q29) by A19, A22, A25, A28, ANPROJ_1: 22;

      consider p299,p39,r19 be Element of V such that

       A33: p2 = ( Dir p299) and

       A34: p3 = ( Dir p39) and

       A35: r1 = ( Dir r19) and

       A36: not p299 is zero and

       A37: not p39 is zero and

       A38: not r19 is zero and

       A39: (p299,p39,r19) are_LinDep by A11, Th23;



       A40: not are_Prop (p39,q39) by A6, A34, A37, A26, A29, ANPROJ_1: 22;

       are_Prop (r199,r19) by A35, A38, A27, A30, ANPROJ_1: 22;

      then

       A41: (q29,q39,r19) are_LinDep by A31, A32, ANPROJ_1: 4;

      consider p199,p399,r29 be Element of V such that

       A42: p1 = ( Dir p199) and

       A43: p3 = ( Dir p399) and

       A44: r2 = ( Dir r29) and

       A45: not p199 is zero and

       A46: not p399 is zero and

       A47: not r29 is zero and

       A48: (p199,p399,r29) are_LinDep by A13, Th23;



       A49: are_Prop (p399,p39) by A34, A37, A43, A46, ANPROJ_1: 22;

      consider o9 be Element of V such that

       A50: not o9 is zero and

       A51: o = ( Dir o9) by ANPROJ_1: 26;



       A52: not are_Prop (o9,q39) by A5, A50, A51, A26, A29, ANPROJ_1: 22;

      consider p19,p29,r39 be Element of V such that

       A53: p1 = ( Dir p19) and

       A54: p2 = ( Dir p29) and

       A55: r3 = ( Dir r39) and

       A56: not p19 is zero and

       A57: not p29 is zero and

       A58: not r39 is zero and

       A59: (p19,p29,r39) are_LinDep by A9, Th23;



       A60: ( not are_Prop (p19,q19)) & not are_Prop (p29,q29) by A2, A4, A53, A54, A56, A57, A18, A19, A21, A22, ANPROJ_1: 22;



       A61: ( not are_Prop (o9,q19)) & not are_Prop (o9,q29) by A1, A3, A50, A51, A18, A19, A21, A22, ANPROJ_1: 22;

      consider o999,p2999,q2999 be Element of V such that

       A62: o = ( Dir o999) and

       A63: p2 = ( Dir p2999) and

       A64: q2 = ( Dir q2999) and

       A65: not o999 is zero and

       A66: not p2999 is zero and

       A67: not q2999 is zero and

       A68: (o999,p2999,q2999) are_LinDep by A16, Th23;



       A69: are_Prop (q2999,q29) by A19, A22, A64, A67, ANPROJ_1: 22;



       A70: are_Prop (o999,o9) by A50, A51, A62, A65, ANPROJ_1: 22;

       are_Prop (p2999,p29) by A54, A57, A63, A66, ANPROJ_1: 22;

      then

       A71: (o9,p29,q29) are_LinDep by A68, A70, A69, ANPROJ_1: 4;

      consider q199,q399,r299 be Element of V such that

       A72: q1 = ( Dir q199) and

       A73: q3 = ( Dir q399) and

       A74: r2 = ( Dir r299) and

       A75: not q199 is zero and

       A76: not q399 is zero and

       A77: not r299 is zero and

       A78: (q199,q399,r299) are_LinDep by A14, Th23;



       A79: are_Prop (q199,q19) by A18, A21, A72, A75, ANPROJ_1: 22;



       A80: not (o9,p19,p29) are_LinDep by A7, A50, A51, A53, A54, A56, A57, Th23;

       are_Prop (r399,r39) by A55, A58, A20, A23, ANPROJ_1: 22;

      then

       A81: (q19,q29,r39) are_LinDep by A24, ANPROJ_1: 4;



       A82: are_Prop (q399,q39) by A26, A29, A73, A76, ANPROJ_1: 22;

      consider o9999,p3999,q3999 be Element of V such that

       A83: o = ( Dir o9999) and

       A84: p3 = ( Dir p3999) and

       A85: q3 = ( Dir q3999) and

       A86: not o9999 is zero and

       A87: not p3999 is zero and

       A88: not q3999 is zero and

       A89: (o9999,p3999,q3999) are_LinDep by A17, Th23;



       A90: are_Prop (q3999,q39) by A26, A29, A85, A88, ANPROJ_1: 22;

       are_Prop (p299,p29) by A54, A57, A33, A36, ANPROJ_1: 22;

      then

       A91: (p29,p39,r19) are_LinDep by A39, ANPROJ_1: 4;

       are_Prop (p199,p19) by A53, A56, A42, A45, ANPROJ_1: 22;

      then (p19,p39,r29) are_LinDep by A48, A49, ANPROJ_1: 4;

      then

       A92: (p19,p29,p39,r19,r29,r39) lie_on_a_triangle by A59, A91;



       A93: (q19,q29,q39) are_Prop_Vect by A21, A22, A29;

      consider o99,p1999,q1999 be Element of V such that

       A94: o = ( Dir o99) and

       A95: p1 = ( Dir p1999) and

       A96: q1 = ( Dir q1999) and

       A97: not o99 is zero and

       A98: not p1999 is zero and

       A99: not q1999 is zero and

       A100: (o99,p1999,q1999) are_LinDep by A15, Th23;



       A101: are_Prop (q1999,q19) by A18, A21, A96, A99, ANPROJ_1: 22;



       A102: ( not (o9,p19,p39) are_LinDep ) & not (o9,p29,p39) are_LinDep by A8, A50, A51, A53, A54, A56, A57, A34, A37, Th23;



       A103: (p19,p29,p39) are_Prop_Vect by A56, A57, A37;



       A104: are_Prop (o9999,o9) by A50, A51, A83, A86, ANPROJ_1: 22;

       are_Prop (p3999,p39) by A34, A37, A84, A87, ANPROJ_1: 22;

      then

       A105: (o9,p39,q39) are_LinDep by A89, A104, A90, ANPROJ_1: 4;



       A106: are_Prop (o99,o9) by A50, A51, A94, A97, ANPROJ_1: 22;

       are_Prop (p1999,p19) by A53, A56, A95, A98, ANPROJ_1: 22;

      then (o9,p19,q19) are_LinDep by A100, A106, A101, ANPROJ_1: 4;

      then

       A107: (o9,p19,p29,p39,q19,q29,q39) are_perspective by A71, A105;

       are_Prop (r299,r29) by A44, A47, A74, A77, ANPROJ_1: 22;

      then (q19,q39,r29) are_LinDep by A78, A79, A82, ANPROJ_1: 4;

      then

       A108: (q19,q29,q39,r19,r29,r39) lie_on_a_triangle by A81, A41;

      (r19,r29,r39) are_Prop_Vect by A58, A38, A47;

      then (r19,r29,r39) are_LinDep by A50, A61, A52, A60, A40, A103, A93, A107, A80, A102, A92, A108, Th8;

      hence thesis by A55, A58, A35, A38, A44, A47, Th23;

    end;



     Lm41: for V be up-3-dimensional RealLinearSpace holds ( ProjectiveSpace V) is Pappian

    proof

      let V be up-3-dimensional RealLinearSpace;

      let o,p1,p2,p3,q1,q2,q3,r1,r2,r3 be Element of ( ProjectiveSpace V);

      assume that

       A1: o <> p2 and

       A2: o <> p3 and

       A3: p2 <> p3 and

       A4: p1 <> p2 and

       A5: p1 <> p3 and

       A6: o <> q2 and

       A7: o <> q3 and

       A8: q2 <> q3 and

       A9: q1 <> q2 and

       A10: q1 <> q3 and

       A11: not (o,p1,q1) are_collinear and

       A12: (o,p1,p2) are_collinear and

       A13: (o,p1,p3) are_collinear and

       A14: (o,q1,q2) are_collinear and

       A15: (o,q1,q3) are_collinear and

       A16: (p1,q2,r3) are_collinear and

       A17: (q1,p2,r3) are_collinear and

       A18: (p1,q3,r2) are_collinear and

       A19: (p3,q1,r2) are_collinear and

       A20: (p2,q3,r1) are_collinear and

       A21: (p3,q2,r1) are_collinear ;

      consider o999,q19,q29 be Element of V such that

       A22: o = ( Dir o999) and

       A23: q1 = ( Dir q19) and

       A24: q2 = ( Dir q29) and

       A25: not o999 is zero and

       A26: not q19 is zero and

       A27: not q29 is zero and

       A28: (o999,q19,q29) are_LinDep by A14, Th23;



       A29: not are_Prop (q19,q29) by A9, A23, A24, A26, A27, ANPROJ_1: 22;

      consider o9999,q199,q39 be Element of V such that

       A30: o = ( Dir o9999) and

       A31: q1 = ( Dir q199) and

       A32: q3 = ( Dir q39) and

       A33: not o9999 is zero and

       A34: not q199 is zero and

       A35: not q39 is zero and

       A36: (o9999,q199,q39) are_LinDep by A15, Th23;



       A37: are_Prop (q199,q19) by A23, A26, A31, A34, ANPROJ_1: 22;

      consider o99,p199,p39 be Element of V such that

       A38: o = ( Dir o99) & p1 = ( Dir p199) and

       A39: p3 = ( Dir p39) and

       A40: not o99 is zero & not p199 is zero and

       A41: not p39 is zero and

       A42: (o99,p199,p39) are_LinDep by A13, Th23;

      consider o9,p19,p29 be Element of V such that

       A43: o = ( Dir o9) and

       A44: p1 = ( Dir p19) and

       A45: p2 = ( Dir p29) and

       A46: not o9 is zero and

       A47: not p19 is zero and

       A48: not p29 is zero and

       A49: (o9,p19,p29) are_LinDep by A12, Th23;



       A50: ( not are_Prop (o9,p39)) & not are_Prop (p19,p39) by A2, A5, A43, A44, A46, A47, A39, A41, ANPROJ_1: 22;



       A51: ( not are_Prop (q19,q39)) & not are_Prop (q29,q39) by A8, A10, A23, A24, A26, A27, A32, A35, ANPROJ_1: 22;



       A52: not are_Prop (p29,p39) by A3, A45, A48, A39, A41, ANPROJ_1: 22;



       A53: not are_Prop (o9,q39) by A7, A43, A46, A32, A35, ANPROJ_1: 22;



       A54: not are_Prop (o9,q29) by A6, A43, A46, A24, A27, ANPROJ_1: 22;

      ( not are_Prop (o9,p29)) & not are_Prop (p19,p29) by A1, A4, A43, A44, A45, A46, A47, A48, ANPROJ_1: 22;

      then

       A55: (o9,p19,p29,p39,q19,q29,q39) are_half_mutually_not_Prop by A54, A53, A50, A29, A52, A51;

      consider q1999,p2999,r399 be Element of V such that

       A56: q1 = ( Dir q1999) and

       A57: p2 = ( Dir p2999) and

       A58: r3 = ( Dir r399) and

       A59: not q1999 is zero and

       A60: not p2999 is zero and

       A61: not r399 is zero and

       A62: (q1999,p2999,r399) are_LinDep by A17, Th23;



       A63: are_Prop (q1999,q19) by A23, A26, A56, A59, ANPROJ_1: 22;

      consider p29999,q3999,r19 be Element of V such that

       A64: p2 = ( Dir p29999) and

       A65: q3 = ( Dir q3999) and

       A66: r1 = ( Dir r19) and

       A67: not p29999 is zero and

       A68: not q3999 is zero and

       A69: not r19 is zero and

       A70: (p29999,q3999,r19) are_LinDep by A20, Th23;



       A71: are_Prop (q3999,q39) by A32, A35, A65, A68, ANPROJ_1: 22;

       are_Prop (o999,o9) by A43, A46, A22, A25, ANPROJ_1: 22;

      then

       A72: (o9,q19,q29) are_LinDep by A28, ANPROJ_1: 4;

       are_Prop (o9999,o9) by A43, A46, A30, A33, ANPROJ_1: 22;

      then

       A73: (o9,q19,q39) are_LinDep by A36, A37, ANPROJ_1: 4;

       are_Prop (o99,o9) & are_Prop (p199,p19) by A43, A44, A46, A47, A38, A40, ANPROJ_1: 22;

      then

       A74: (o9,p19,p39) are_LinDep by A42, ANPROJ_1: 4;

       not (o9,p19,q19) are_LinDep by A11, A43, A44, A46, A47, A23, A26, Th23;

      then

       A75: (o9,p19,p29,p39,q19,q29,q39) lie_on_an_angle by A49, A74, A72, A73;

      consider p19999,q399,r29 be Element of V such that

       A76: p1 = ( Dir p19999) and

       A77: q3 = ( Dir q399) and

       A78: r2 = ( Dir r29) and

       A79: not p19999 is zero and

       A80: not q399 is zero and

       A81: not r29 is zero and

       A82: (p19999,q399,r29) are_LinDep by A18, Th23;



       A83: are_Prop (q399,q39) by A32, A35, A77, A80, ANPROJ_1: 22;

      consider p3999,q29999,r199 be Element of V such that

       A84: p3 = ( Dir p3999) and

       A85: q2 = ( Dir q29999) and

       A86: r1 = ( Dir r199) and

       A87: not p3999 is zero and

       A88: not q29999 is zero and

       A89: not r199 is zero and

       A90: (p3999,q29999,r199) are_LinDep by A21, Th23;



       A91: are_Prop (p3999,p39) by A39, A41, A84, A87, ANPROJ_1: 22;



       A92: are_Prop (q29999,q29) by A24, A27, A85, A88, ANPROJ_1: 22;

       are_Prop (r199,r19) by A66, A69, A86, A89, ANPROJ_1: 22;

      then

       A93: (p39,q29,r19) are_LinDep by A90, A91, A92, ANPROJ_1: 4;



       A94: (q19,q29,q39) are_Prop_Vect by A26, A27, A35;



       A95: (p19,p29,p39) are_Prop_Vect by A47, A48, A41;

       are_Prop (p29999,p29) by A45, A48, A64, A67, ANPROJ_1: 22;

      then

       A96: (p29,q39,r19) are_LinDep by A70, A71, ANPROJ_1: 4;

      consider p399,q1999,r299 be Element of V such that

       A97: p3 = ( Dir p399) and

       A98: q1 = ( Dir q1999) and

       A99: r2 = ( Dir r299) and

       A100: not p399 is zero and

       A101: not q1999 is zero and

       A102: not r299 is zero and

       A103: (p399,q1999,r299) are_LinDep by A19, Th23;



       A104: are_Prop (q1999,q19) by A23, A26, A98, A101, ANPROJ_1: 22;

       are_Prop (p19999,p19) by A44, A47, A76, A79, ANPROJ_1: 22;

      then

       A105: (p19,q39,r29) are_LinDep by A82, A83, ANPROJ_1: 4;

      consider p1999,q2999,r39 be Element of V such that

       A106: p1 = ( Dir p1999) and

       A107: q2 = ( Dir q2999) and

       A108: r3 = ( Dir r39) and

       A109: not p1999 is zero and

       A110: not q2999 is zero and

       A111: not r39 is zero and

       A112: (p1999,q2999,r39) are_LinDep by A16, Th23;



       A113: are_Prop (q2999,q29) by A24, A27, A107, A110, ANPROJ_1: 22;



       A114: are_Prop (p2999,p29) by A45, A48, A57, A60, ANPROJ_1: 22;

       are_Prop (r399,r39) by A108, A111, A58, A61, ANPROJ_1: 22;

      then

       A115: (q19,p29,r39) are_LinDep by A62, A63, A114, ANPROJ_1: 4;

       are_Prop (p1999,p19) by A44, A47, A106, A109, ANPROJ_1: 22;

      then

       A116: (p19,q29,r39) are_LinDep by A112, A113, ANPROJ_1: 4;



       A117: are_Prop (p399,p39) by A39, A41, A97, A100, ANPROJ_1: 22;

       are_Prop (r299,r29) by A78, A81, A99, A102, ANPROJ_1: 22;

      then

       A118: (p39,q19,r29) are_LinDep by A103, A117, A104, ANPROJ_1: 4;

      (r19,r29,r39) are_Prop_Vect by A111, A81, A69;

      then (r19,r29,r39) are_LinDep by A46, A75, A55, A95, A94, A116, A115, A105, A118, A96, A93, Th9;

      hence thesis by A108, A111, A78, A81, A66, A69, Th23;

    end;

    registration

      let V be up-3-dimensional RealLinearSpace;

      ::$Notion-Name

      cluster ( ProjectiveSpace V) -> Fanoian Desarguesian Pappian;

      coherence by Lm39, Lm40, Lm41;

    end

    theorem :: ANPROJ_2:27



     Th27: (ex u, v, w st (for a, b, c st (((a * u) + (b * v)) + (c * w)) = ( 0. V) holds a = 0 & b = 0 & c = 0 ) & (for y holds ex a, b, c st y = (((a * u) + (b * v)) + (c * w)))) implies ex x1,x2 be Element of ( ProjectiveSpace V) st (x1 <> x2 & for r1, r2 holds ex q st (x1,x2,q) are_collinear & (r1,r2,q) are_collinear )

    proof

      given p,q,r be Element of V such that

       A1: for a, b, c st (((a * p) + (b * q)) + (c * r)) = ( 0. V) holds a = 0 & b = 0 & c = 0 and

       A2: for y holds ex a, b, c st y = (((a * p) + (b * q)) + (c * r));



       A3: not p is zero & not q is zero by A1, Th1;

      then

      reconsider x1 = ( Dir p), x2 = ( Dir q) as Element of ( ProjectiveSpace V) by ANPROJ_1: 26;

      take x1, x2;

       not are_Prop (p,q) by A1, Th1;

      hence x1 <> x2 by A3, ANPROJ_1: 22;

      let r1, r2;

      consider u such that

       A4: not u is zero & r1 = ( Dir u) by ANPROJ_1: 26;

      consider u1 such that

       A5: not u1 is zero & r2 = ( Dir u1) by ANPROJ_1: 26;

      consider y such that

       A6: (p,q,y) are_LinDep and

       A7: (u,u1,y) are_LinDep and

       A8: not y is zero by A1, A2, Th3;

      reconsider q = ( Dir y) as Element of ( ProjectiveSpace V) by A8, ANPROJ_1: 26;

      take q;

      thus (x1,x2,q) are_collinear by A3, A6, A8, Th23;

      thus thesis by A4, A5, A7, A8, Th23;

    end;

    theorem :: ANPROJ_2:28



     Th28: (ex x1,x2 be Element of ( ProjectiveSpace V) st (x1 <> x2 & for r1, r2 holds ex q st (x1,x2,q) are_collinear & (r1,r2,q) are_collinear )) implies for p, p1, q, q1 holds ex r st (p,p1,r) are_collinear & (q,q1,r) are_collinear

    proof

      given x1,x2 be Element of ( ProjectiveSpace V) such that

       A1: x1 <> x2 and

       A2: for r1, r2 holds ex q st (x1,x2,q) are_collinear & (r1,r2,q) are_collinear ;

      let p, p1, q, q1;

      consider p3 be Element of ( ProjectiveSpace V) such that

       A3: (x1,x2,p3) are_collinear and

       A4: (p,p1,p3) are_collinear by A2;

      consider q3 be Element of ( ProjectiveSpace V) such that

       A5: (x1,x2,q3) are_collinear and

       A6: (q,q1,q3) are_collinear by A2;

      consider s2 be Element of ( ProjectiveSpace V) such that

       A7: (x1,x2,s2) are_collinear and

       A8: (p,q,s2) are_collinear by A2;



       A9: (s2,p,q) are_collinear by A8, Th24;

      consider s4 be Element of ( ProjectiveSpace V) such that

       A10: (x1,x2,s4) are_collinear and

       A11: (p,q1,s4) are_collinear by A2;



       A12: (s4,q1,p) are_collinear by A11, Th24;

      (p3,s2,q3) are_collinear by A1, A3, A5, A7, Def8;

      then

      consider s3 be Element of ( ProjectiveSpace V) such that

       A13: (p3,p,s3) are_collinear and

       A14: (q3,q,s3) are_collinear by A9, Def9;

      consider s be Element of ( ProjectiveSpace V) such that

       A15: (x1,x2,s) are_collinear and

       A16: (p1,q1,s) are_collinear by A2;

      (q3,s4,p3) are_collinear by A1, A3, A5, A10, Def8;

      then

      consider s5 be Element of ( ProjectiveSpace V) such that

       A17: (q3,q1,s5) are_collinear and

       A18: (p3,p,s5) are_collinear by A12, Def9;



       A19: (p1,s,q1) are_collinear by A16, Th24;

      consider s6 be Element of ( ProjectiveSpace V) such that

       A20: (x1,x2,s6) are_collinear and

       A21: (p1,q,s6) are_collinear by A2;



       A22: (s6,p1,q) are_collinear by A21, Th24;

      (p3,s6,q3) are_collinear by A1, A3, A5, A20, Def8;

      then

      consider s7 be Element of ( ProjectiveSpace V) such that

       A23: (p3,p1,s7) are_collinear and

       A24: (q3,q,s7) are_collinear by A22, Def9;

      (s,p3,q3) are_collinear by A1, A3, A5, A15, Def8;

      then

      consider s1 be Element of ( ProjectiveSpace V) such that

       A25: (p1,p3,s1) are_collinear and

       A26: (q1,q3,s1) are_collinear by A19, Def9;

       A27:

      now

         A28:

        now



           A29: (q3,q1,s1) are_collinear by A26, Th24;

          assume that

           A30: p3 <> p1 and

           A31: q3 <> q1;

          (q3,q1,q) are_collinear & (q3,q1,q1) are_collinear by A6, Def7, Th24;

          then

           A32: (q,q1,s1) are_collinear by A31, A29, Def8;

          take s1;



           A33: (p3,p1,s1) are_collinear by A25, Th24;

          (p3,p1,p) are_collinear & (p3,p1,p1) are_collinear by A4, Def7, Th24;

          then (p,p1,s1) are_collinear by A30, A33, Def8;

          hence thesis by A32;

        end;

         A34:

        now

          assume that

           A35: p3 <> p and

           A36: q3 <> q;

          take s3;

          (q3,q,q) are_collinear & (q3,q,q1) are_collinear by A6, Def7, Th24;

          then

           A37: (q,q1,s3) are_collinear by A14, A36, Def8;

          (p3,p,p) are_collinear & (p3,p,p1) are_collinear by A4, Def7, Th24;

          then (p,p1,s3) are_collinear by A13, A35, Def8;

          hence thesis by A37;

        end;

         A38:

        now

          assume that

           A39: p3 <> p1 and

           A40: q3 <> q;

          take s7;

          (q3,q,q) are_collinear & (q3,q,q1) are_collinear by A6, Def7, Th24;

          then

           A41: (q,q1,s7) are_collinear by A24, A40, Def8;

          (p3,p1,p) are_collinear & (p3,p1,p1) are_collinear by A4, Def7, Th24;

          then (p,p1,s7) are_collinear by A23, A39, Def8;

          hence thesis by A41;

        end;

         A42:

        now

          assume that

           A43: p3 <> p and

           A44: q3 <> q1;

          take s5;

          (q3,q1,q) are_collinear & (q3,q1,q1) are_collinear by A6, Def7, Th24;

          then

           A45: (q,q1,s5) are_collinear by A17, A44, Def8;

          (p3,p,p) are_collinear & (p3,p,p1) are_collinear by A4, Def7, Th24;

          then (p,p1,s5) are_collinear by A18, A43, Def8;

          hence thesis by A45;

        end;

        assume p <> p1 & q <> q1;

        hence thesis by A34, A42, A38, A28;

      end;

      now

         A46:

        now

          assume

           A47: p = p1;

          take q3;

          (p,p1,q3) are_collinear by A47, Def7;

          hence thesis by A6;

        end;

         A48:

        now

          assume

           A49: q = q1;

          take p3;

          (q,q1,p3) are_collinear by A49, Def7;

          hence thesis by A4;

        end;

        assume p = p1 or q = q1;

        hence thesis by A48, A46;

      end;

      hence thesis by A27;

    end;

    theorem :: ANPROJ_2:29



     Th29: (ex u, v, w st (for a, b, c st (((a * u) + (b * v)) + (c * w)) = ( 0. V) holds a = 0 & b = 0 & c = 0 ) & (for y holds ex a, b, c st y = (((a * u) + (b * v)) + (c * w)))) implies ex CS be CollProjectiveSpace st CS = ( ProjectiveSpace V) & CS is 2-dimensional

    proof

      given u, v, w such that

       A1: for a, b, c st (((a * u) + (b * v)) + (c * w)) = ( 0. V) holds a = 0 & b = 0 & c = 0 and

       A2: for y holds ex a, b, c st y = (((a * u) + (b * v)) + (c * w));

      reconsider V9 = V as up-3-dimensional RealLinearSpace by A1, Def6;

      take ( ProjectiveSpace V9);

      ex x1,x2 be Element of ( ProjectiveSpace V) st (x1 <> x2 & for r1, r2 holds ex q st (x1,x2,q) are_collinear & (r1,r2,q) are_collinear ) by A1, A2, Th27;

      then for p, p1, q, q1 holds ex r st (p,p1,r) are_collinear & (q,q1,r) are_collinear by Th28;

      hence thesis;

    end;



     Lm42: (ex y, u, v, w st (for a, b, a1, b1 st ((((a * y) + (b * u)) + (a1 * v)) + (b1 * w)) = ( 0. V) holds a = 0 & b = 0 & a1 = 0 & b1 = 0 )) implies V is up-3-dimensional

    proof

      given y, u, v, w such that

       A1: for a, b, a1, b1 st ((((a * y) + (b * u)) + (a1 * v)) + (b1 * w)) = ( 0. V) holds a = 0 & b = 0 & a1 = 0 & b1 = 0 ;

      take y, u, v;

      let a, b, a1;

      assume (((a * y) + (b * u)) + (a1 * v)) = ( 0. V);



      then ( 0. V) = ((((a * y) + (b * u)) + (a1 * v)) + ( 0. V)) by RLVECT_1: 4

      .= ((((a * y) + (b * u)) + (a1 * v)) + ( 0 * w)) by RLVECT_1: 10;

      hence thesis by A1;

    end;



     Lm43: (ex y, u, v, w st (for a, b, a1, b1 st ((((a * y) + (b * u)) + (a1 * v)) + (b1 * w)) = ( 0. V) holds a = 0 & b = 0 & a1 = 0 & b1 = 0 )) implies ( ProjectiveSpace V) is proper at_least_3rank

    proof

      given y, u, v, w such that

       A1: for a, b, a1, b1 st ((((a * y) + (b * u)) + (a1 * v)) + (b1 * w)) = ( 0. V) holds a = 0 & b = 0 & a1 = 0 & b1 = 0 ;

      V is up-3-dimensional by A1, Lm42;

      hence thesis;

    end;

    theorem :: ANPROJ_2:30



     Th30: (ex y, u, v, w st (for w1 holds ex a, b, a1, b1 st w1 = ((((a * y) + (b * u)) + (a1 * v)) + (b1 * w))) & (for a, b, a1, b1 st ((((a * y) + (b * u)) + (a1 * v)) + (b1 * w)) = ( 0. V) holds a = 0 & b = 0 & a1 = 0 & b1 = 0 )) implies ex p, q1, q2 st not (p,q1,q2) are_collinear & for r1, r2 holds ex q3, r3 st (r1,r2,r3) are_collinear & (q1,q2,q3) are_collinear & (p,r3,q3) are_collinear

    proof

      given y, u, v, w such that

       A1: for w1 holds ex a, b, a1, b1 st w1 = ((((a * y) + (b * u)) + (a1 * v)) + (b1 * w)) and

       A2: for a, b, a1, b1 st ((((a * y) + (b * u)) + (a1 * v)) + (b1 * w)) = ( 0. V) holds a = 0 & b = 0 & a1 = 0 & b1 = 0 ;



       A3: not u is zero & not v is zero by A2, Th2;



       A4: not y is zero by A2, Th2;

      then

      reconsider p = ( Dir y), q1 = ( Dir u), q2 = ( Dir v) as Element of ( ProjectiveSpace V) by A3, ANPROJ_1: 26;

      take p, q1, q2;

       not (y,u,v) are_LinDep by A2, Th2;

      then not (p,q1,q2) are_collinear by A4, A3, ANPROJ_1: 25;

      hence not (p,q1,q2) are_collinear ;

      let r1, r2;

      consider u1 such that

       A5: not u1 is zero and

       A6: r1 = ( Dir u1) by ANPROJ_1: 26;

      consider u2 such that

       A7: not u2 is zero and

       A8: r2 = ( Dir u2) by ANPROJ_1: 26;

      consider w1, w2 such that

       A9: (u1,u2,w2) are_LinDep and

       A10: (u,v,w1) are_LinDep and

       A11: (y,w2,w1) are_LinDep and

       A12: not w1 is zero and

       A13: not w2 is zero by A1, A2, A5, A7, Th4;

      reconsider q3 = ( Dir w1), r3 = ( Dir w2) as Element of ( ProjectiveSpace V) by A12, A13, ANPROJ_1: 26;

      take q3, r3;

      thus (r1,r2,r3) are_collinear by A5, A6, A7, A8, A9, A13, Th23;

      thus (q1,q2,q3) are_collinear by A3, A10, A12, Th23;

      thus thesis by A4, A11, A12, A13, Th23;

    end;



     Lm44: for x,d,b,b9,d9,q be Element of ( ProjectiveSpace V) st not (q,b,d) are_collinear & (b,d,x) are_collinear & (q,b9,b) are_collinear & (q,d9,d) are_collinear holds ex o be Element of ( ProjectiveSpace V) st (b9,d9,o) are_collinear & (q,x,o) are_collinear

    proof

      let x,d,b,b9,d9,q be Element of ( ProjectiveSpace V);

      assume that

       A1: not (q,b,d) are_collinear and

       A2: (b,d,x) are_collinear and

       A3: (q,b9,b) are_collinear and

       A4: (q,d9,d) are_collinear ;



       A5: (b9,q,b) are_collinear by A3, Th24;



       A6: b <> d by A1, Def7;

       A7:

      now



         A8: (b,b9,q) are_collinear by A3, Th24;

        consider z be Element of ( ProjectiveSpace V) such that

         A9: (b9,d9,z) are_collinear and

         A10: (b,d,z) are_collinear by A4, A5, Def9;



         A11: (z,b9,b9) are_collinear by Def7;

        (b,d,b) are_collinear by Def7;

        then (z,b,x) are_collinear by A2, A6, A10, Def8;

        then

        consider o be Element of ( ProjectiveSpace V) such that

         A12: (z,b9,o) are_collinear and

         A13: (x,q,o) are_collinear by A8, Def9;



         A14: (q,x,o) are_collinear by A13, Th24;

        assume

         A15: b <> b9;



         A16: z <> b9

        proof

          assume not thesis;

          then

           A17: (b,b9,d) are_collinear by A10, Th24;

          (b,b9,q) are_collinear & (b,b9,b) are_collinear by A3, Def7, Th24;

          hence contradiction by A1, A15, A17, Def8;

        end;

        (z,b9,d9) are_collinear by A9, Th24;

        then (b9,d9,o) are_collinear by A12, A16, A11, Def8;

        hence thesis by A14;

      end;

      now

        assume b = b9;

        then

         A18: (d,b9,x) are_collinear by A2, Th24;

        (d9,d,q) are_collinear by A4, Th24;

        then

        consider o be Element of ( ProjectiveSpace V) such that

         A19: (d9,b9,o) are_collinear and

         A20: (q,x,o) are_collinear by A18, Def9;

        (b9,d9,o) are_collinear by A19, Th24;

        hence thesis by A20;

      end;

      hence thesis by A7;

    end;

    reserve x,z,x1,y1,z1,x2,x3,y2,z2,p4,q4 for Element of ( ProjectiveSpace V);

    theorem :: ANPROJ_2:31



     Th31: ( ProjectiveSpace V) is proper at_least_3rank & (ex p, q1, q2 st not (p,q1,q2) are_collinear & (for r1, r2 holds ex q3, r3 st (r1,r2,r3) are_collinear & (q1,q2,q3) are_collinear & (p,r3,q3) are_collinear )) implies ex CS be CollProjectiveSpace st CS = ( ProjectiveSpace V) & CS is at_most-3-dimensional

    proof

      assume that

       A1: ( ProjectiveSpace V) is proper and

       A2: for p, q holds ex r st p <> r & q <> r & (p,q,r) are_collinear ;

      defpred P[ Element of ( ProjectiveSpace V), Element of ( ProjectiveSpace V), Element of ( ProjectiveSpace V)] means for y1, y2 holds ex x2, x1 st (y1,y2,x1) are_collinear & ($2,$3,x2) are_collinear & ($1,x1,x2) are_collinear ;



       A3: for p, q1, q2 st (q1,q2,p) are_collinear holds P[p, q1, q2]

      proof

        let p, q1, q2 such that

         A4: (q1,q2,p) are_collinear ;

        now

          let y1, y2;

          (y1,y2,y2) are_collinear & (p,y2,p) are_collinear by Def7;

          hence ex x2, x1 st (y1,y2,x1) are_collinear & (q1,q2,x2) are_collinear & (p,x1,x2) are_collinear by A4;

        end;

        hence thesis;

      end;



       A5: for q, q1, q2, p1, p2, x st P[q, q1, q2] & not (q1,q2,q) are_collinear & (q1,q2,x) are_collinear & not (p1,p2,q) are_collinear & (p1,p2,x) are_collinear holds P[q, p1, p2]

      proof

        let q, q1, q2, p1, p2, x;

        assume that

         A6: P[q, q1, q2] and

         A7: not (q1,q2,q) are_collinear and

         A8: (q1,q2,x) are_collinear and

         A9: not (p1,p2,q) are_collinear and

         A10: (p1,p2,x) are_collinear ;



         A11: q1 <> q2 by A7, Def7;



         A12: p1 <> p2 by A9, Def7;

        now

          let y1, y2;

           A13:

          now

            ex a be Element of ( ProjectiveSpace V) st (p1,p2,a) are_collinear & x <> a

            proof

               A14:

              now

                assume

                 A15: x <> p2;

                take p2;

                (p1,p2,p2) are_collinear by Def7;

                hence thesis by A15;

              end;

              now

                assume

                 A16: x <> p1;

                take p1;

                (p1,p2,p1) are_collinear by Def7;

                hence thesis by A16;

              end;

              hence thesis by A9, A14, Def7;

            end;

            then

            consider x1 such that

             A17: (p1,p2,x1) are_collinear and

             A18: x <> x1;

            consider b,b9 be Element of ( ProjectiveSpace V) such that

             A19: (y1,y2,b9) are_collinear and

             A20: (q1,q2,b) are_collinear and

             A21: (q,b9,b) are_collinear by A6;

            assume

             A22: y1 <> y2;

            ex a be Element of ( ProjectiveSpace V) st (y1,y2,a) are_collinear & b9 <> a

            proof

               A23:

              now

                assume

                 A24: b9 <> y2;

                take y2;

                (y1,y2,y2) are_collinear by Def7;

                hence thesis by A24;

              end;

              now

                assume

                 A25: b9 <> y1;

                take y1;

                (y1,y2,y1) are_collinear by Def7;

                hence thesis by A25;

              end;

              hence thesis by A22, A23;

            end;

            then

            consider x3 such that

             A26: b9 <> x3 and

             A27: (y1,y2,x3) are_collinear ;

            consider d,d9 be Element of ( ProjectiveSpace V) such that

             A28: (x1,x3,d9) are_collinear and

             A29: (q1,q2,d) are_collinear and

             A30: (q,d9,d) are_collinear by A6;



             A31: (b,d,x) are_collinear by A8, A11, A20, A29, Def8;

             A32:

            now

              assume

               A33: b <> d;

               not (q,b,d) are_collinear

              proof

                (q1,q2,q2) are_collinear by Def7;

                then

                 A34: (b,d,q2) are_collinear by A11, A20, A29, Def8;

                assume not thesis;

                then

                 A35: (b,d,q) are_collinear by Th24;

                (q1,q2,q1) are_collinear by Def7;

                then (b,d,q1) are_collinear by A11, A20, A29, Def8;

                hence contradiction by A7, A33, A35, A34, Def8;

              end;

              then

              consider o be Element of ( ProjectiveSpace V) such that

               A36: (b9,d9,o) are_collinear and

               A37: (q,x,o) are_collinear by A21, A30, A31, Lm44;



               A38: (o,x,q) are_collinear by A37, Th24;

              (d9,x3,x1) are_collinear by A28, Th24;

              then

              consider z1 such that

               A39: (b9,x3,z1) are_collinear and

               A40: (o,x1,z1) are_collinear by A36, Def9;

              (x1,o,z1) are_collinear by A40, Th24;

              then

              consider z2 such that

               A41: (x1,x,z2) are_collinear and

               A42: (z1,q,z2) are_collinear by A38, Def9;



               A43: (q,z1,z2) are_collinear by A42, Th24;

              (p1,p2,p2) are_collinear by Def7;

              then

               A44: (x1,x,p2) are_collinear by A10, A12, A17, Def8;

              (y1,y2,y2) are_collinear by Def7;

              then

               A45: (b9,x3,y2) are_collinear by A22, A19, A27, Def8;

              (p1,p2,p1) are_collinear by Def7;

              then (x1,x,p1) are_collinear by A10, A12, A17, Def8;

              then

               A46: (p1,p2,z2) are_collinear by A18, A41, A44, Def8;

              (y1,y2,y1) are_collinear by Def7;

              then (b9,x3,y1) are_collinear by A22, A19, A27, Def8;

              then (y1,y2,z1) are_collinear by A26, A39, A45, Def8;

              hence ex z2, z1 st (y1,y2,z1) are_collinear & (p1,p2,z2) are_collinear & (q,z1,z2) are_collinear by A46, A43;

            end;

            now

              assume b = d;

              then

               A47: (b,q,d9) are_collinear by A30, Th24;

              (y1,y2,y2) are_collinear by Def7;

              then

               A48: (b9,x3,y2) are_collinear by A22, A19, A27, Def8;



               A49: (d9,x3,x1) are_collinear by A28, Th24;

              (b,q,b9) are_collinear & (b,q,q) are_collinear by A21, Def7, Th24;

              then (b9,d9,q) are_collinear by A7, A20, A47, Def8;

              then

              consider z1 such that

               A50: (b9,x3,z1) are_collinear and

               A51: (q,x1,z1) are_collinear by A49, Def9;



               A52: (q,z1,x1) are_collinear by A51, Th24;

              (y1,y2,y1) are_collinear by Def7;

              then (b9,x3,y1) are_collinear by A22, A19, A27, Def8;

              then (y1,y2,z1) are_collinear by A26, A50, A48, Def8;

              hence ex z2, z1 st (y1,y2,z1) are_collinear & (p1,p2,z2) are_collinear & (q,z1,z2) are_collinear by A17, A52;

            end;

            hence ex z2, z1 st (y1,y2,z1) are_collinear & (p1,p2,z2) are_collinear & (q,z1,z2) are_collinear by A32;

          end;

          now

            assume y1 = y2;

            then

             A53: (y1,y2,q) are_collinear by Def7;

            (p1,p2,p1) are_collinear & (q,q,p1) are_collinear by Def7;

            hence ex z2, z1 st (y1,y2,z1) are_collinear & (p1,p2,z2) are_collinear & (q,z1,z2) are_collinear by A53;

          end;

          hence ex z2, z1 st (y1,y2,z1) are_collinear & (p1,p2,z2) are_collinear & (q,z1,z2) are_collinear by A13;

        end;

        hence thesis;

      end;



       A54: for q1, q2, p1, p2, q st not (q1,q2,q) are_collinear & not (p1,p2,q) are_collinear & ( not ex x st ((q1,q2,x) are_collinear & (p1,p2,x) are_collinear )) holds ex q3, p3 st (p1,p2,p3) are_collinear & (q1,q2,q3) are_collinear & not (q3,p3,q) are_collinear

      proof

        let q1, q2, p1, p2, q such that

         A55: not (q1,q2,q) are_collinear and

         A56: not (p1,p2,q) are_collinear and not ex x st ((q1,q2,x) are_collinear & (p1,p2,x) are_collinear );



         A57: q <> q1 by A55, Def7;



         A58: not (q1,p1,q) are_collinear or not (q1,p2,q) are_collinear

        proof

          assume not thesis;

          then

           A59: (q,q1,p1) are_collinear & (q,q1,p2) are_collinear by Th24;

          (q,q1,q) are_collinear by Def7;

          hence contradiction by A56, A57, A59, Def8;

        end;



         A60: (p1,p2,p2) are_collinear by Def7;

        (q1,q2,q1) are_collinear & (p1,p2,p1) are_collinear by Def7;

        hence thesis by A60, A58;

      end;



       A61: for q, q1, q2, p1, p2 st P[q, q1, q2] & not (q1,q2,q) are_collinear & not (p1,p2,q) are_collinear & not ex x st ((q1,q2,x) are_collinear & (p1,p2,x) are_collinear ) holds P[q, p1, p2]

      proof

        let q, q1, q2, p1, p2;

        assume that

         A62: P[q, q1, q2] and

         A63: not (q1,q2,q) are_collinear and

         A64: not (p1,p2,q) are_collinear and

         A65: not ex x st ((q1,q2,x) are_collinear & (p1,p2,x) are_collinear );

        consider q3, p3 such that

         A66: (p1,p2,p3) are_collinear and

         A67: (q1,q2,q3) are_collinear and

         A68: not (q3,p3,q) are_collinear by A54, A63, A64, A65;

        (q3,p3,q3) are_collinear by Def7;

        then

         A69: P[q, q3, p3] by A5, A62, A63, A67, A68;

        (q3,p3,p3) are_collinear by Def7;

        hence thesis by A5, A64, A66, A68, A69;

      end;



       A70: for q, q1, q2 st P[q, q1, q2] & not (q1,q2,q) are_collinear holds for p1, p2 holds P[q, p1, p2]

      proof

        let q, q1, q2 such that

         A71: P[q, q1, q2] & not (q1,q2,q) are_collinear ;

        let p1, p2;



         A72: not (p1,p2,q) are_collinear & ( not ex x st (q1,q2,x) are_collinear & (p1,p2,x) are_collinear ) implies P[q, p1, p2] by A61, A71;

         not (p1,p2,q) are_collinear & (ex x st (q1,q2,x) are_collinear & (p1,p2,x) are_collinear ) implies P[q, p1, p2] by A5, A71;

        hence thesis by A3, A72;

      end;

      reconsider CS = ( ProjectiveSpace V) as CollProjectiveSpace by A1, A2, Def10;

      given p, q1, q2 such that

       A73: not (p,q1,q2) are_collinear and

       A74: for r1, r2 holds ex q3, r3 st (r1,r2,r3) are_collinear & (q1,q2,q3) are_collinear & (p,r3,q3) are_collinear ;

      take CS;



       A75: for q, q1, q2, x, q3 st P[q, q1, q2] & not (q1,q2,q) are_collinear & (q1,q2,x) are_collinear & (q,q3,x) are_collinear holds P[q3, q1, q2]

      proof

        let q, q1, q2, x, q3 such that

         A76: P[q, q1, q2] and

         A77: not (q1,q2,q) are_collinear and

         A78: (q1,q2,x) are_collinear and

         A79: (q,q3,x) are_collinear ;

        now

          let y1, y2;

          consider z2, z1 such that

           A80: (y1,y2,z1) are_collinear and

           A81: (q1,q2,z2) are_collinear and

           A82: (q,z1,z2) are_collinear by A76;

           A83:

          now

            (q3,q,x) are_collinear by A79, Th24;

            then

            consider x2 such that

             A84: (q3,z1,x2) are_collinear and

             A85: (x,z2,x2) are_collinear by A82, Def9;



             A86: q1 <> q2 by A77, Def7;

            (q1,q2,q2) are_collinear by Def7;

            then

             A87: (x,z2,q2) are_collinear by A78, A81, A86, Def8;

            (q1,q2,q1) are_collinear by Def7;

            then

             A88: (x,z2,q1) are_collinear by A78, A81, A86, Def8;

            assume x <> z2;

            then (q1,q2,x2) are_collinear by A85, A88, A87, Def8;

            hence ex x2, x1 st (y1,y2,x1) are_collinear & (q1,q2,x2) are_collinear & (q3,x1,x2) are_collinear by A80, A84;

          end;

          now



             A89: (q,x,q3) are_collinear & (q,x,x) are_collinear by A79, Def7, Th24;

            assume

             A90: x = z2;

            then (q,x,z1) are_collinear by A82, Th24;

            then (q3,z1,z2) are_collinear by A77, A78, A90, A89, Def8;

            hence ex x2, x1 st (y1,y2,x1) are_collinear & (q1,q2,x2) are_collinear & (q3,x1,x2) are_collinear by A80, A81;

          end;

          hence ex x2, x1 st (y1,y2,x1) are_collinear & (q1,q2,x2) are_collinear & (q3,x1,x2) are_collinear by A83;

        end;

        hence thesis;

      end;



       A91: for q, p holds ((for q1, q2 holds P[q, q1, q2]) implies ex p1, p2 st P[p, p1, p2] & not (p1,p2,p) are_collinear )

      proof

        let q, p such that

         A92: for q1, q2 holds P[q, q1, q2];

        consider x1 such that

         A93: p <> x1 and

         A94: q <> x1 and

         A95: (p,q,x1) are_collinear by A2;

        consider x2 such that

         A96: not (p,x1,x2) are_collinear by A1, A93, COLLSP: 12;



         A97: not (x1,x2,q) are_collinear

        proof

          assume not thesis;

          then

           A98: (q,x1,x2) are_collinear by Th24;

          (q,x1,x1) are_collinear & (q,x1,p) are_collinear by A95, Def7, Th24;

          hence contradiction by A94, A96, A98, Def8;

        end;



         A99: (x1,x2,x1) are_collinear by Def7;



         A100: not (x1,x2,p) are_collinear by A96, Th24;



         A101: P[q, x1, x2] by A92;

        (q,p,x1) are_collinear by A95, Th24;

        then P[p, x1, x2] by A75, A97, A99, A101;

        hence thesis by A100;

      end;



       A102: for x, y1, z holds P[x, y1, z]

      proof

        let x, y1, z;

         not (q1,q2,p) are_collinear by A73, Th24;

        then for p1, p2 holds P[p, p1, p2] by A74, A70;

        then ex r1, r2 st P[x, r1, r2] & not (r1,r2,x) are_collinear by A91;

        hence thesis by A70;

      end;

      for p4, p1, q, q4, r2 holds ex r, r1 st (p4,q,r) are_collinear & (p1,q4,r1) are_collinear & (r2,r,r1) are_collinear

      proof

        let p4, p1, q, q4, r2;

        ex r1, r st (p4,q,r) are_collinear & (p1,q4,r1) are_collinear & (r2,r,r1) are_collinear by A102;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: ANPROJ_2:32



     Th32: (ex y, u, v, w st (for w1 holds ex a, b, c, c1 st w1 = ((((a * y) + (b * u)) + (c * v)) + (c1 * w))) & (for a, b, a1, b1 st ((((a * y) + (b * u)) + (a1 * v)) + (b1 * w)) = ( 0. V) holds a = 0 & b = 0 & a1 = 0 & b1 = 0 )) implies ex CS be CollProjectiveSpace st CS = ( ProjectiveSpace V) & CS is at_most-3-dimensional

    proof

      given y, u, v, w such that

       A1: (for w1 holds ex a, b, c, c1 st w1 = ((((a * y) + (b * u)) + (c * v)) + (c1 * w))) & for a, b, a1, b1 st ((((a * y) + (b * u)) + (a1 * v)) + (b1 * w)) = ( 0. V) holds a = 0 & b = 0 & a1 = 0 & b1 = 0 ;

      ( ProjectiveSpace V) is proper at_least_3rank & ex p, q1, q2 st not (p,q1,q2) are_collinear & for r1, r2 holds ex q3, r3 st (r1,r2,r3) are_collinear & (q1,q2,q3) are_collinear & (p,r3,q3) are_collinear by A1, Lm43, Th30;

      hence thesis by Th31;

    end;

    theorem :: ANPROJ_2:33



     Th33: (ex u, v, u1, v1 st (for a, b, a1, b1 st ((((a * u) + (b * v)) + (a1 * u1)) + (b1 * v1)) = ( 0. V) holds a = 0 & b = 0 & a1 = 0 & b1 = 0 )) implies ex CS be CollProjectiveSpace st CS = ( ProjectiveSpace V) & CS is non 2-dimensional

    proof

      given u, v, u1, v1 such that

       A1: for a, b, a1, b1 st ((((a * u) + (b * v)) + (a1 * u1)) + (b1 * v1)) = ( 0. V) holds a = 0 & b = 0 & a1 = 0 & b1 = 0 ;

      V is up-3-dimensional by A1, Lm42;

      then

      reconsider CS = ( ProjectiveSpace V) as CollProjectiveSpace;

      take CS;

      thus CS = ( ProjectiveSpace V);



       A2: not u1 is zero & not v1 is zero by A1, Th2;



       A3: not u is zero & not v is zero by A1, Th2;

      then

      reconsider p = ( Dir u), p1 = ( Dir v), q = ( Dir u1), q1 = ( Dir v1) as Element of CS by A2, ANPROJ_1: 26;

      take p, p1, q, q1;

      thus not ex r be Element of CS st ((p,p1,r) are_collinear & (q,q1,r) are_collinear )

      proof

        assume not thesis;

        then

        consider r be Element of CS such that

         A4: (p,p1,r) are_collinear and

         A5: (q,q1,r) are_collinear ;

        consider y such that

         A6: not y is zero and

         A7: r = ( Dir y) by ANPROJ_1: 26;

         [q, q1, r] in the Collinearity of ( ProjectiveSpace V) by A5;

        then

         A8: (u1,v1,y) are_LinDep by A2, A6, A7, ANPROJ_1: 25;

         [p, p1, r] in the Collinearity of ( ProjectiveSpace V) by A4;

        then (u,v,y) are_LinDep by A3, A6, A7, ANPROJ_1: 25;

        hence contradiction by A1, A6, A8, Th5;

      end;

    end;

    theorem :: ANPROJ_2:34



     Th34: (ex u, v, u1, v1 st (for w holds ex a, b, a1, b1 st w = ((((a * u) + (b * v)) + (a1 * u1)) + (b1 * v1))) & (for a, b, a1, b1 st ((((a * u) + (b * v)) + (a1 * u1)) + (b1 * v1)) = ( 0. V) holds a = 0 & b = 0 & a1 = 0 & b1 = 0 )) implies ex CS be CollProjectiveSpace st CS = ( ProjectiveSpace V) & CS is up-3-dimensional at_most-3-dimensional

    proof

      assume ex u, v, u1, v1 st (for w holds ex a, b, a1, b1 st w = ((((a * u) + (b * v)) + (a1 * u1)) + (b1 * v1))) & for a, b, a1, b1 st ((((a * u) + (b * v)) + (a1 * u1)) + (b1 * v1)) = ( 0. V) holds a = 0 & b = 0 & a1 = 0 & b1 = 0 ;

      then (ex CS1 be CollProjectiveSpace st CS1 = ( ProjectiveSpace V) & CS1 is up-3-dimensional) & ex CS2 be CollProjectiveSpace st CS2 = ( ProjectiveSpace V) & CS2 is at_most-3-dimensional by Th32, Th33;

      hence thesis;

    end;

    registration

      cluster strict Fanoian Desarguesian Pappian 2-dimensional for CollProjectiveSpace;

      existence

      proof

        consider V be non trivial RealLinearSpace such that

         A1: ex u,v,w be Element of V st (for a, b, c st (((a * u) + (b * v)) + (c * w)) = ( 0. V) holds a = 0 & b = 0 & c = 0 ) & for y be Element of V holds ex a, b, c st y = (((a * u) + (b * v)) + (c * w)) by Th16;

        reconsider V as up-3-dimensional RealLinearSpace by A1, Def6;

        take CS = ( ProjectiveSpace V);

        thus CS is strict Fanoian Desarguesian Pappian;

        ex CS1 be CollProjectiveSpace st CS1 = ( ProjectiveSpace V) & CS1 is 2-dimensional by A1, Th29;

        hence thesis;

      end;

      cluster strict Fanoian Desarguesian Pappian at_most-3-dimensional up-3-dimensional for CollProjectiveSpace;

      existence

      proof

        consider V be non trivial RealLinearSpace such that

         A2: ex u,v,w,u1 be Element of V st (for a, b, c, d st ((((a * u) + (b * v)) + (c * w)) + (d * u1)) = ( 0. V) holds a = 0 & b = 0 & c = 0 & d = 0 ) & for y be Element of V holds ex a, b, c, d st y = ((((a * u) + (b * v)) + (c * w)) + (d * u1)) by Th22;

        reconsider V as up-3-dimensional RealLinearSpace by A2, Lm42;

        take CS = ( ProjectiveSpace V);

        thus CS is strict Fanoian Desarguesian Pappian;

        ex CS be CollProjectiveSpace st CS = ( ProjectiveSpace V) & CS is up-3-dimensional at_most-3-dimensional by A2, Th34;

        hence thesis;

      end;

    end

    definition

      mode CollProjectivePlane is 2-dimensional CollProjectiveSpace;

    end

    theorem :: ANPROJ_2:35

    for CS be non empty CollStr holds CS is 2-dimensional CollProjectiveSpace iff (CS is at_least_3rank proper CollSp & for p,p1,q,q1 be Element of CS holds ex r be Element of CS st (p,p1,r) are_collinear & (q,q1,r) are_collinear )

    proof

      let CS be non empty CollStr;

      thus CS is 2-dimensional CollProjectiveSpace implies CS is at_least_3rank proper CollSp & for p,p1,q,q1 be Element of CS holds ex r be Element of CS st (p,p1,r) are_collinear & (q,q1,r) are_collinear by Def14;

      assume that

       A1: CS is at_least_3rank proper CollSp and

       A2: for p,p1,q,q1 be Element of CS holds ex r be Element of CS st (p,p1,r) are_collinear & (q,q1,r) are_collinear ;

      CS is Vebleian by A2;

      hence thesis by A1, A2, Def14;

    end;