symsp_1.miz



    begin

    reserve F for Field;

    definition

      let F;

      struct ( RelStr, ModuleStr over F) SymStr over F (# the carrier -> set,

the addF -> BinOp of the carrier,

the ZeroF -> Element of the carrier,

the lmult -> Function of [:the carrier of F, the carrier:], the carrier,

the InternalRel -> Relation of the carrier #)

       attr strict strict;

    end

    registration

      let F;

      cluster non empty for SymStr over F;

      existence

      proof

        set X = the non empty set, a = the BinOp of X, Z = the Element of X, l = the Function of [:the carrier of F, X:], X, r = the Relation of X;

        take SymStr (# X, a, Z, l, r #);

        thus the carrier of SymStr (# X, a, Z, l, r #) is non empty;

      end;

    end

    notation

      let F;

      let S be SymStr over F;

      let a,b be Element of S;

      synonym a _|_ b for a <= b;

    end

    set X = { 0 };

    reconsider o = 0 as Element of { 0 } by TARSKI:def 1;

    deffunc F( Element of { 0 }, Element of { 0 }) = o;

    consider md be BinOp of { 0 } such that

     Lm1: for x,y be Element of { 0 } holds (md . (x,y)) = F(x,y) from BINOP_1:sch 4;

     Lm2:

    now

      defpred P[ object] means ex a,b be Element of X st $1 = [a, b] & b = o;

      set CV = [:X, X:];

      let F;

      consider mo be set such that

       A1: for x be object holds x in mo iff x in CV & P[x] from XBOOLE_0:sch 1;

      mo c= CV by A1;

      then

      reconsider mo as Relation of X;

      take mo;

      thus for x be set holds x in mo iff x in CV & ex a,b be Element of X st x = [a, b] & b = o by A1;

    end;

    registration

      let F;

      let X be non empty set, md be BinOp of X, o be Element of X, mF be Function of [:the carrier of F, X:], X, mo be Relation of X;

      cluster SymStr (# X, md, o, mF, mo #) -> non empty;

      coherence ;

    end

    

     Lm3: for mF be Function of [:the carrier of F, X:], X, mo be Relation of X holds SymStr (# X, md, o, mF, mo #) is Abelian add-associative right_zeroed right_complementable

    proof

      let mF be Function of [:the carrier of F, X:], X;

      let mo be Relation of X;

      set H = SymStr (# X, md, o, mF, mo #);

      thus H is Abelian

      proof

        let x,y be Element of H;

        reconsider x, y as Element of X;

        (md . (x,y)) = o by Lm1;

        hence thesis by Lm1;

      end;

      thus H is add-associative

      proof

        let x,y,z be Element of H;

        reconsider x, y, z as Element of X;

        (md . (x,(md . (y,z)))) = o by Lm1;

        hence thesis by Lm1;

      end;

      thus H is right_zeroed

      proof

        let x be Element of H;

        reconsider x as Element of X;

        (md . (x,( 0. H))) = o by Lm1;

        hence thesis by TARSKI:def 1;

      end;

      let x be Element of H;

      take ( - x);

      thus thesis by Lm1;

    end;

    registration

      let F;

      cluster Abelian add-associative right_zeroed right_complementable for non empty SymStr over F;

      existence

      proof

        set mo = the Relation of X;

        set mF = the Function of [:the carrier of F, X:], X;

         SymStr (# X, md, o, mF, mo #) is Abelian add-associative right_zeroed right_complementable by Lm3;

        hence thesis;

      end;

    end

     Lm4:

    now

      let F;

      let mF be Function of [:the carrier of F, X:], X such that

       A1: for a be Element of F holds for x be Element of X holds (mF . (a,x)) = o;

      let mo be Relation of X;

      let MPS be Abelian add-associative right_zeroed right_complementable non empty SymStr over F such that

       A2: MPS = SymStr (# X, md, o, mF, mo #);

      for x,y be Element of F holds for v,w be Element of MPS holds (x * (v + w)) = ((x * v) + (x * w)) & ((x + y) * v) = ((x * v) + (y * v)) & ((x * y) * v) = (x * (y * v)) & (( 1_ F) * v) = v

      proof

        let x,y be Element of F;

        let v,w be Element of MPS;

        

         A3: ((x * y) * v) = (x * (y * v))

        proof

          set z = (x * y);

          

           A4: (z * v) = (mF . (z,v)) by A2, VECTSP_1:def 12;

          reconsider v as Element of MPS;

          reconsider v as Element of MPS;

          

           A5: ((x * y) * v) = o by A1, A2, A4;

          reconsider v as Element of MPS;

          

           A6: (mF . (y,v)) = o by A1, A2;

          reconsider v as Element of MPS;

          (y * v) = o by A2, A6, VECTSP_1:def 12;

          then (x * (y * v)) = (mF . (x,o)) by A2, VECTSP_1:def 12;

          hence thesis by A1, A5;

        end;

        

         A7: (x * (v + w)) = ((x * v) + (x * w))

        proof

          reconsider v, w as Element of X by A2;

          

           A8: (md . (v,w)) = o by Lm1;

          reconsider v, w as Element of MPS;

          (x * (v + w)) = (mF . (x,o)) by A2, A8, VECTSP_1:def 12;

          then

           A9: (x * (v + w)) = o by A1;

          (mF . (x,v)) = o by A1;

          then

           A10: (x * v) = o by A2, VECTSP_1:def 12;

          (mF . (x,w)) = o by A1;

          then

           A11: (x * w) = o by A2, VECTSP_1:def 12;

          o = ( 0. MPS) by A2;

          hence thesis by A9, A10, A11, RLVECT_1: 4;

        end;

        

         A12: ((x + y) * v) = ((x * v) + (y * v))

        proof

          set z = (x + y);

          

           A13: (z * v) = (mF . (z,v)) by A2, VECTSP_1:def 12;

          reconsider v as Element of MPS;

          reconsider v as Element of MPS;

          

           A14: ((x + y) * v) = o by A1, A2, A13;

          reconsider v as Element of MPS;

          

           A15: (mF . (x,v)) = o by A1, A2;

          reconsider v as Element of MPS;

          

           A16: (x * v) = o by A2, A15, VECTSP_1:def 12;

          reconsider v as Element of MPS;

          

           A17: (mF . (y,v)) = o by A1, A2;

          

           A18: o = ( 0. MPS) by A2;

          reconsider v as Element of MPS;

          (y * v) = o by A2, A17, VECTSP_1:def 12;

          hence thesis by A14, A16, A18, RLVECT_1: 4;

        end;

        (( 1_ F) * v) = v

        proof

          set one1 = ( 1_ F);

          

           A19: (one1 * v) = (mF . (one1,v)) by A2, VECTSP_1:def 12;

          reconsider v as Element of MPS;

          (mF . (one1,v)) = o by A1, A2;

          hence thesis by A2, A19, TARSKI:def 1;

        end;

        hence thesis by A7, A12, A3;

      end;

      hence MPS is vector-distributive scalar-distributive scalar-associative scalar-unital by VECTSP_1:def 14, VECTSP_1:def 15, VECTSP_1:def 16, VECTSP_1:def 17;

    end;

     Lm5:

    now

      set CV = [:X, X:];

      let F;

      let mF be Function of [:the carrier of F, X:], X;

      let mo be Relation of X such that

       A1: for x be set holds x in mo iff x in CV & ex a,b be Element of X st x = [a, b] & b = o;

      let MPS be Abelian add-associative right_zeroed right_complementable non empty SymStr over F such that

       A2: MPS = SymStr (# X, md, o, mF, mo #);

      thus for a be Element of MPS holds (a <> ( 0. MPS) implies ex p be Element of MPS st not p _|_ a) by A2, TARSKI:def 1;

      

       A3: for a,b be Element of MPS holds a _|_ b iff [a, b] in CV & ex c,d be Element of X st [a, b] = [c, d] & d = o

      proof

        let a,b be Element of MPS;

        a _|_ b iff [a, b] in mo by A2, ORDERS_2:def 5;

        hence thesis by A1;

      end;

      

       A4: for a,b be Element of MPS holds a _|_ b iff b = o

      proof

        let a,b be Element of MPS;

        

         A5: b = o implies a _|_ b

        proof

          consider c,d be Element of MPS such that

           A6: c = a & d = b;

          assume

           A7: b = o;

           [a, b] = [c, d] by A6;

          hence thesis by A2, A3, A7;

        end;

        a _|_ b implies b = o

        proof

          assume a _|_ b;

          then ex c,d be Element of X st [a, b] = [c, d] & d = o by A3;

          hence thesis by XTUPLE_0: 1;

        end;

        hence thesis by A5;

      end;

      thus for a,b be Element of MPS holds for l be Element of F holds (a _|_ b implies (l * a) _|_ b)

      proof

        let a,b be Element of MPS;

        let l be Element of F;

        assume a _|_ b;

        then b = o by A4;

        hence thesis by A4;

      end;

      thus for a,b,c be Element of MPS holds (b _|_ a & c _|_ a implies (b + c) _|_ a)

      proof

        let a,b,c be Element of MPS;

        assume that

         A8: b _|_ a and c _|_ a;

        a = o by A4, A8;

        hence thesis by A4;

      end;

      thus for a,b,x be Element of MPS holds ( not b _|_ a implies ex k be Element of F st (x - (k * b)) _|_ a)

      proof

        let a,b,x be Element of MPS;

        assume

         A9: not b _|_ a;

        assume not thesis;

        a <> o by A4, A9;

        hence contradiction by A2, TARSKI:def 1;

      end;

      let a,b,c be Element of MPS;

      assume that a _|_ (b + c) and b _|_ (c + a);

      assume not c _|_ (a + b);

      then (a + b) <> o by A4;

      hence contradiction by A2, TARSKI:def 1;

    end;

    definition

      let F;

      let IT be Abelian add-associative right_zeroed right_complementable non empty SymStr over F;

      :: SYMSP_1:def1

      attr IT is SymSp-like means

      : Def1: for a,b,c,x be Element of IT holds for l be Element of F holds (a <> ( 0. IT) implies ex y be Element of IT st not y _|_ a) & (a _|_ b implies (l * a) _|_ b) & (b _|_ a & c _|_ a implies (b + c) _|_ a) & ( not b _|_ a implies ex k be Element of F st (x - (k * b)) _|_ a) & (a _|_ (b + c) & b _|_ (c + a) implies c _|_ (a + b));

    end

    registration

      let F;

      cluster SymSp-like vector-distributive scalar-distributive scalar-associative scalar-unital strict for Abelian add-associative right_zeroed right_complementable non empty SymStr over F;

      existence

      proof

        deffunc F( Element of F, Element of X) = o;

        consider mF be Function of [:the carrier of F, X:], X such that

         A1: for a be Element of F holds for x be Element of X holds (mF . (a,x)) = F(a,x) from BINOP_1:sch 4;

        consider mo be Relation of X such that

         A2: for x be set holds x in mo iff x in [:X, X:] & ex a,b be Element of X st x = [a, b] & b = o by Lm2;

        reconsider MPS = SymStr (# X, md, o, mF, mo #) as Abelian add-associative right_zeroed right_complementable non empty SymStr over F by Lm3;

        take MPS;

        thus for a,b,c,x be Element of MPS holds for l be Element of F holds (a <> ( 0. MPS) implies ex y be Element of MPS st not y _|_ a) & (a _|_ b implies (l * a) _|_ b) & (b _|_ a & c _|_ a implies (b + c) _|_ a) & ( not b _|_ a implies ex k be Element of F st (x - (k * b)) _|_ a) & (a _|_ (b + c) & b _|_ (c + a) implies c _|_ (a + b)) by A2, Lm5;

        thus MPS is vector-distributive scalar-distributive scalar-associative scalar-unital by A1, Lm4;

        thus thesis;

      end;

    end

    definition

      let F;

      mode SymSp of F is SymSp-like vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable non empty SymStr over F;

    end

    reserve S for SymSp of F;

    reserve a,b,c,d,a9,b9,p,q,r,s,x,y,z for Element of S;

    reserve k,l for Element of F;

    theorem :: SYMSP_1:1

    

     Th1: ( 0. S) _|_ a

    proof

      set 0V = ( 0. S), 0F = ( 0. F);

       A1:

      now

        assume not a _|_ a;

        then

        consider m be Element of F such that

         A2: (0V - (m * a)) _|_ a by Def1;

        (0F * (0V - (m * a))) _|_ a by A2, Def1;

        hence thesis by VECTSP_1: 14;

      end;

      now

        assume a _|_ a;

        then (0F * a) _|_ a by Def1;

        hence thesis by VECTSP_1: 14;

      end;

      hence thesis by A1;

    end;

    theorem :: SYMSP_1:2

    

     Th2: a _|_ b implies b _|_ a

    proof

      set 0V = ( 0. S);

      assume a _|_ b;

      then

       A1: a _|_ (0V + b) by RLVECT_1: 4;

      0V _|_ (b + a) by Th1;

      then b _|_ (a + 0V) by A1, Def1;

      hence thesis by RLVECT_1: 4;

    end;

    theorem :: SYMSP_1:3

    

     Th3: not a _|_ b & (c + a) _|_ b implies not c _|_ b

    proof

      assume that

       A1: not a _|_ b and

       A2: (c + a) _|_ b;

      assume not thesis;

      then (( - ( 1_ F)) * c) _|_ b by Def1;

      then ( - c) _|_ b by VECTSP_1: 14;

      then (( - c) + (c + a)) _|_ b by A2, Def1;

      then ((c + ( - c)) + a) _|_ b by RLVECT_1:def 3;

      then (( 0. S) + a) _|_ b by RLVECT_1: 5;

      hence contradiction by A1, RLVECT_1: 4;

    end;

    theorem :: SYMSP_1:4

    

     Th4: not b _|_ a & c _|_ a implies not (b + c) _|_ a

    proof

      assume that

       A1: not b _|_ a and

       A2: c _|_ a;

      (( - ( 1_ F)) * c) _|_ a by A2, Def1;

      then

       A3: ( - c) _|_ a by VECTSP_1: 14;

      assume not thesis;

      then ((b + c) + ( - c)) _|_ a by A3, Def1;

      then (b + (c + ( - c))) _|_ a by RLVECT_1:def 3;

      then (b + ( 0. S)) _|_ a by RLVECT_1: 5;

      hence contradiction by A1, RLVECT_1: 4;

    end;

    theorem :: SYMSP_1:5

    

     Th5: not b _|_ a & not l = ( 0. F) implies not (l * b) _|_ a & not b _|_ (l * a)

    proof

      set 1F = ( 1. F);

      assume that

       A1: not b _|_ a and

       A2: not l = ( 0. F);

       A3:

      now

        consider k such that

         A4: (k * l) = 1F by A2, VECTSP_1:def 9;

        assume b _|_ (l * a);

        then (l * a) _|_ b by Th2;

        then (k * (l * a)) _|_ b by Def1;

        then (1F * a) _|_ b by A4, VECTSP_1:def 16;

        then a _|_ b by VECTSP_1:def 17;

        hence contradiction by A1, Th2;

      end;

      now

        consider k such that

         A5: (k * l) = 1F by A2, VECTSP_1:def 9;

        assume (l * b) _|_ a;

        then (k * (l * b)) _|_ a by Def1;

        then (1F * b) _|_ a by A5, VECTSP_1:def 16;

        hence contradiction by A1, VECTSP_1:def 17;

      end;

      hence thesis by A3;

    end;

    theorem :: SYMSP_1:6

    

     Th6: a _|_ b implies ( - a) _|_ b

    proof

      assume a _|_ b;

      then (( - ( 1_ F)) * a) _|_ b by Def1;

      hence thesis by VECTSP_1: 14;

    end;

    theorem :: SYMSP_1:7

    

     Th7: not a _|_ c implies not (a + b) _|_ c or not (((( 1_ F) + ( 1_ F)) * a) + b) _|_ c

    proof

      set 1F = ( 1_ F);

      assume

       A1: not a _|_ c;

      assume

       A2: not thesis;

      then (((1F * a) + (( 1_ F) * a)) + b) _|_ c by VECTSP_1:def 15;

      then ((a + (1F * a)) + b) _|_ c by VECTSP_1:def 17;

      then ((a + a) + b) _|_ c by VECTSP_1:def 17;

      then (a + (a + b)) _|_ c by RLVECT_1:def 3;

      hence contradiction by A1, A2, Th4;

    end;

    theorem :: SYMSP_1:8

    

     Th8: not a9 _|_ a & a9 _|_ b & not b9 _|_ b & b9 _|_ a implies not (a9 + b9) _|_ a & not (a9 + b9) _|_ b

    proof

      set 0V = ( 0. S);

      assume that

       A1: not a9 _|_ a and

       A2: a9 _|_ b and

       A3: not b9 _|_ b and

       A4: b9 _|_ a;

      assume not thesis;

      then (a9 + b9) _|_ a & (( - ( 1_ F)) * b9) _|_ a or (a9 + b9) _|_ b & (( - ( 1_ F)) * a9) _|_ b by A2, A4, Def1;

      then (a9 + b9) _|_ a & ( - b9) _|_ a or (a9 + b9) _|_ b & ( - a9) _|_ b by VECTSP_1: 14;

      then ((a9 + b9) + ( - b9)) _|_ a or (( - a9) + (a9 + b9)) _|_ b by Def1;

      then (a9 + (b9 + ( - b9))) _|_ a or ((( - a9) + a9) + b9) _|_ b by RLVECT_1:def 3;

      then (a9 + 0V) _|_ a or (0V + b9) _|_ b by RLVECT_1: 5;

      hence contradiction by A1, A3, RLVECT_1: 4;

    end;

    theorem :: SYMSP_1:9

    

     Th9: a <> ( 0. S) & b <> ( 0. S) implies ex p st not p _|_ a & not p _|_ b

    proof

      assume that

       A1: a <> ( 0. S) and

       A2: b <> ( 0. S);

      consider a9 such that

       A3: not a9 _|_ a by A1, Def1;

      now

        consider b9 such that

         A4: not b9 _|_ b by A2, Def1;

        assume

         A5: a9 _|_ b;

        now

          assume b9 _|_ a;

          then ( not (a9 + b9) _|_ a) & not (a9 + b9) _|_ b by A3, A5, A4, Th8;

          hence thesis;

        end;

        hence thesis by A4;

      end;

      hence thesis by A3;

    end;

    theorem :: SYMSP_1:10

    

     Th10: (( 1_ F) + ( 1_ F)) <> ( 0. F) & a <> ( 0. S) & b <> ( 0. S) & c <> ( 0. S) implies ex p st not p _|_ a & not p _|_ b & not p _|_ c

    proof

      assume that

       A1: (( 1_ F) + ( 1_ F)) <> ( 0. F) and

       A2: a <> ( 0. S) and

       A3: b <> ( 0. S) and

       A4: c <> ( 0. S);

      consider r such that

       A5: not r _|_ a and

       A6: not r _|_ b by A2, A3, Th9;

      consider s such that

       A7: not s _|_ a and

       A8: not s _|_ c by A2, A4, Th9;

      now

        assume that

         A9: r _|_ c and

         A10: s _|_ b;

         A11:

        now

          ((( 1_ F) + ( 1_ F)) * r) _|_ c by A9, Def1;

          then

           A12: not (((( 1_ F) + ( 1_ F)) * r) + s) _|_ c by A8, Th4;

           not ((( 1_ F) + ( 1_ F)) * r) _|_ b by A1, A6, Th5;

          then

           A13: not (((( 1_ F) + ( 1_ F)) * r) + s) _|_ b by A10, Th4;

          assume not (((( 1_ F) + ( 1_ F)) * r) + s) _|_ a;

          hence thesis by A13, A12;

        end;

        now

          assume

           A14: not (r + s) _|_ a;

          ( not (r + s) _|_ b) & not (r + s) _|_ c by A6, A8, A9, A10, Th4;

          hence thesis by A14;

        end;

        hence thesis by A5, A11, Th7;

      end;

      hence thesis by A5, A6, A7, A8;

    end;

    theorem :: SYMSP_1:11

    

     Th11: (a - b) _|_ d & (a - c) _|_ d implies (b - c) _|_ d

    proof

      assume that

       A1: (a - b) _|_ d and

       A2: (a - c) _|_ d;

      ( - (a - b)) _|_ d by A1, Th6;

      then (( - a) + b) _|_ d by VECTSP_1: 17;

      then ((b + ( - a)) + (a - c)) _|_ d by A2, Def1;

      then (b + (( - a) + (a - c))) _|_ d by RLVECT_1:def 3;

      then (b + ((( - a) + a) + ( - c))) _|_ d by RLVECT_1:def 3;

      then (b + (( 0. S) + ( - c))) _|_ d by RLVECT_1: 5;

      hence thesis by RLVECT_1: 4;

    end;

    theorem :: SYMSP_1:12

    

     Th12: not b _|_ a & (x - (k * b)) _|_ a & (x - (l * b)) _|_ a implies k = l

    proof

      assume that

       A1: not b _|_ a and

       A2: (x - (k * b)) _|_ a & (x - (l * b)) _|_ a;

      set 1F = ( 1_ F);

      ((k * b) - (l * b)) _|_ a by A2, Th11;

      then ((k * b) + (( - 1F) * (l * b))) _|_ a by VECTSP_1: 14;

      then ((k * b) + ((( - 1F) * l) * b)) _|_ a by VECTSP_1:def 16;

      then ((k * b) + (( - (l * 1F)) * b)) _|_ a by VECTSP_1: 9;

      then ((k * b) + (( - l) * b)) _|_ a;

      then ((k + ( - l)) * b) _|_ a by VECTSP_1:def 15;

      then (((k + ( - l)) " ) * ((k + ( - l)) * b)) _|_ a by Def1;

      then

       A3: ((((k + ( - l)) " ) * (k + ( - l))) * b) _|_ a by VECTSP_1:def 16;

      assume not thesis;

      then (k - l) <> ( 0. F) by RLVECT_1: 21;

      then (1F * b) _|_ a by A3, VECTSP_1:def 10;

      hence contradiction by A1, VECTSP_1:def 17;

    end;

    theorem :: SYMSP_1:13

    

     Th13: (( 1_ F) + ( 1_ F)) <> ( 0. F) implies a _|_ a

    proof

      set 1F = ( 1_ F);

      assume

       A1: (( 1_ F) + ( 1_ F)) <> ( 0. F);

      now

        assume a <> ( 0. S);

        then

        consider c such that

         A2: not c _|_ a by Def1;

        consider k such that

         A3: (a - (k * c)) _|_ a by A2, Def1;

        a _|_ (a + ( - (k * c))) by A3, Th2;

        then ( - (k * c)) _|_ (a + a) by Def1;

        then ( - (k * c)) _|_ (a + (1F * a)) by VECTSP_1:def 17;

        then ( - (k * c)) _|_ ((1F * a) + (1F * a)) by VECTSP_1:def 17;

        then (( - 1F) * (k * c)) _|_ ((1F * a) + (1F * a)) by VECTSP_1: 14;

        then (( - 1F) * (k * c)) _|_ ((1F + 1F) * a) by VECTSP_1:def 15;

        then ((( - 1F) * k) * c) _|_ ((1F + 1F) * a) by VECTSP_1:def 16;

        then (( - (k * 1F)) * c) _|_ ((1F + 1F) * a) by VECTSP_1: 9;

        then (( - k) * c) _|_ ((( 1_ F) + 1F) * a);

        then ((( 1_ F) + ( 1_ F)) * a) _|_ (( - k) * c) by Th2;

        then (((( 1_ F) + ( 1_ F)) " ) * ((( 1_ F) + ( 1_ F)) * a)) _|_ (( - k) * c) by Def1;

        then a _|_ (( - k) * c) by A1, VECTSP_1: 20;

        then

         A4: (( - k) * c) _|_ a by Th2;

        (a + (( - k) * c)) _|_ a by A3, VECTSP_1: 21;

        hence thesis by A4, Th4;

      end;

      hence thesis by Th1;

    end;

    definition

      let F;

      let S, a, b, x;

      assume

       A1: not b _|_ a;

      :: SYMSP_1:def2

      func ProJ (a,b,x) -> Element of F means

      : Def2: for l be Element of F st (x - (l * b)) _|_ a holds it = l;

      existence

      proof

        consider k be Element of F such that

         A2: (x - (k * b)) _|_ a by A1, Def1;

        take k;

        let l be Element of F;

        assume (x - (l * b)) _|_ a;

        hence thesis by A1, A2, Th12;

      end;

      uniqueness

      proof

        let l1,l2 be Element of F such that

         A3: for l be Element of F st (x - (l * b)) _|_ a holds l1 = l and

         A4: for l be Element of F st (x - (l * b)) _|_ a holds l2 = l;

        consider k be Element of F such that

         A5: (x - (k * b)) _|_ a by A1, Def1;

        l1 = k by A3, A5;

        hence thesis by A4, A5;

      end;

    end

    theorem :: SYMSP_1:14

    

     Th14: not b _|_ a implies (x - (( ProJ (a,b,x)) * b)) _|_ a

    proof

      assume

       A1: not b _|_ a;

      then ex l be Element of F st (x - (l * b)) _|_ a by Def1;

      hence thesis by A1, Def2;

    end;

    theorem :: SYMSP_1:15

    

     Th15: not b _|_ a implies ( ProJ (a,b,(l * x))) = (l * ( ProJ (a,b,x)))

    proof

      set L = (x - (( ProJ (a,b,x)) * b));

      

       A1: (l * L) = ((l * x) - (l * (( ProJ (a,b,x)) * b))) by VECTSP_1: 23

      .= ((l * x) - ((l * ( ProJ (a,b,x))) * b)) by VECTSP_1:def 16;

      assume

       A2: not b _|_ a;

      then

       A3: ((l * x) - (( ProJ (a,b,(l * x))) * b)) _|_ a by Th14;

      L _|_ a by A2, Th14;

      then ((l * x) - ((l * ( ProJ (a,b,x))) * b)) _|_ a by A1, Def1;

      hence thesis by A2, A3, Th12;

    end;

    theorem :: SYMSP_1:16

    

     Th16: not b _|_ a implies ( ProJ (a,b,(x + y))) = (( ProJ (a,b,x)) + ( ProJ (a,b,y)))

    proof

      set 1F = ( 1_ F);

      set L = ((x - (( ProJ (a,b,x)) * b)) + (y - (( ProJ (a,b,y)) * b)));

      

       A1: L = (((( - (( ProJ (a,b,x)) * b)) + x) + y) + ( - (( ProJ (a,b,y)) * b))) by RLVECT_1:def 3

      .= (((x + y) + ( - (( ProJ (a,b,x)) * b))) + ( - (( ProJ (a,b,y)) * b))) by RLVECT_1:def 3

      .= ((x + y) + (( - (( ProJ (a,b,x)) * b)) + ( - (( ProJ (a,b,y)) * b)))) by RLVECT_1:def 3

      .= ((x + y) + ((1F * ( - (( ProJ (a,b,x)) * b))) + ( - (( ProJ (a,b,y)) * b)))) by VECTSP_1:def 17

      .= ((x + y) + ((1F * ( - (( ProJ (a,b,x)) * b))) + (1F * ( - (( ProJ (a,b,y)) * b))))) by VECTSP_1:def 17

      .= ((x + y) + ((1F * (( - ( ProJ (a,b,x))) * b)) + (1F * ( - (( ProJ (a,b,y)) * b))))) by VECTSP_1: 21

      .= ((x + y) + ((1F * (( - ( ProJ (a,b,x))) * b)) + (1F * (( - ( ProJ (a,b,y))) * b)))) by VECTSP_1: 21

      .= ((x + y) + (((1F * ( - ( ProJ (a,b,x)))) * b) + (1F * (( - ( ProJ (a,b,y))) * b)))) by VECTSP_1:def 16

      .= ((x + y) + (((( - ( ProJ (a,b,x))) * 1F) * b) + ((1F * ( - ( ProJ (a,b,y)))) * b))) by VECTSP_1:def 16

      .= ((x + y) + ((( - ( ProJ (a,b,x))) * b) + ((( - ( ProJ (a,b,y))) * 1F) * b)))

      .= ((x + y) + ((( - ( ProJ (a,b,x))) * b) + (( - ( ProJ (a,b,y))) * b)))

      .= ((x + y) + ((( - ( ProJ (a,b,x))) + ( - ( ProJ (a,b,y)))) * b)) by VECTSP_1:def 15

      .= ((x + y) + (( - (( ProJ (a,b,x)) + ( ProJ (a,b,y)))) * b)) by RLVECT_1: 31

      .= ((x + y) - ((( ProJ (a,b,x)) + ( ProJ (a,b,y))) * b)) by VECTSP_1: 21;

      assume

       A2: not b _|_ a;

      then (x - (( ProJ (a,b,x)) * b)) _|_ a & (y - (( ProJ (a,b,y)) * b)) _|_ a by Th14;

      then

       A3: L _|_ a by Def1;

      ((x + y) - (( ProJ (a,b,(x + y))) * b)) _|_ a by A2, Th14;

      hence thesis by A2, A3, A1, Th12;

    end;

    theorem :: SYMSP_1:17

     not b _|_ a & l <> ( 0. F) implies ( ProJ (a,(l * b),x)) = ((l " ) * ( ProJ (a,b,x)))

    proof

      assume that

       A1: not b _|_ a and

       A2: l <> ( 0. F);

      set L = (x - (( ProJ (a,(l * b),x)) * (l * b)));

       not (l * b) _|_ a by A1, A2, Th5;

      then

       A3: L _|_ a by Th14;

      

       A4: L = (x - ((( ProJ (a,(l * b),x)) * l) * b)) by VECTSP_1:def 16;

      (x - (( ProJ (a,b,x)) * b)) _|_ a by A1, Th14;

      then (( ProJ (a,b,x)) * (l " )) = ((( ProJ (a,(l * b),x)) * l) * (l " )) by A1, A3, A4, Th12;

      then (( ProJ (a,b,x)) * (l " )) = (( ProJ (a,(l * b),x)) * (l * (l " ))) by GROUP_1:def 3;

      then ((l " ) * ( ProJ (a,b,x))) = (( ProJ (a,(l * b),x)) * ( 1_ F)) by A2, VECTSP_1:def 10;

      hence thesis;

    end;

    theorem :: SYMSP_1:18

    

     Th18: not b _|_ a & l <> ( 0. F) implies ( ProJ ((l * a),b,x)) = ( ProJ (a,b,x))

    proof

      assume that

       A1: not b _|_ a and

       A2: l <> ( 0. F);

       not b _|_ (l * a) by A1, A2, Th5;

      then (x - (( ProJ ((l * a),b,x)) * b)) _|_ (l * a) by Th14;

      then (l * a) _|_ (x - (( ProJ ((l * a),b,x)) * b)) by Th2;

      then ((l " ) * (l * a)) _|_ (x - (( ProJ ((l * a),b,x)) * b)) by Def1;

      then (((l " ) * l) * a) _|_ (x - (( ProJ ((l * a),b,x)) * b)) by VECTSP_1:def 16;

      then (( 1_ F) * a) _|_ (x - (( ProJ ((l * a),b,x)) * b)) by A2, VECTSP_1:def 10;

      then a _|_ (x - (( ProJ ((l * a),b,x)) * b)) by VECTSP_1:def 17;

      then

       A3: (x - (( ProJ ((l * a),b,x)) * b)) _|_ a by Th2;

      (x - (( ProJ (a,b,x)) * b)) _|_ a by A1, Th14;

      hence thesis by A1, A3, Th12;

    end;

    theorem :: SYMSP_1:19

    

     Th19: not b _|_ a & p _|_ a implies ( ProJ (a,(b + p),c)) = ( ProJ (a,b,c)) & ( ProJ (a,b,(c + p))) = ( ProJ (a,b,c))

    proof

      set 0V = ( 0. S);

      assume that

       A1: not b _|_ a and

       A2: p _|_ a;

       not (b + p) _|_ a by A1, A2, Th4;

      then (c - (( ProJ (a,(b + p),c)) * (b + p))) _|_ a by Th14;

      then (c - ((( ProJ (a,(b + p),c)) * b) + (( ProJ (a,(b + p),c)) * p))) _|_ a by VECTSP_1:def 14;

      then

       A3: ((c - (( ProJ (a,(b + p),c)) * b)) - (( ProJ (a,(b + p),c)) * p)) _|_ a by VECTSP_1: 17;

      ((c + p) - (( ProJ (a,b,(c + p))) * b)) _|_ a & ( - p) _|_ a by A1, A2, Th6, Th14;

      then (( - p) + ((p + c) - (( ProJ (a,b,(c + p))) * b))) _|_ a by Def1;

      then (( - p) + (p + (c + ( - (( ProJ (a,b,(c + p))) * b))))) _|_ a by RLVECT_1:def 3;

      then ((( - p) + p) + (c + ( - (( ProJ (a,b,(c + p))) * b)))) _|_ a by RLVECT_1:def 3;

      then (0V + (c + ( - (( ProJ (a,b,(c + p))) * b)))) _|_ a by RLVECT_1: 5;

      then

       A4: (c - (( ProJ (a,b,(c + p))) * b)) _|_ a by RLVECT_1: 4;

      (( ProJ (a,(b + p),c)) * p) _|_ a by A2, Def1;

      then (((c + ( - (( ProJ (a,(b + p),c)) * b))) - (( ProJ (a,(b + p),c)) * p)) + (( ProJ (a,(b + p),c)) * p)) _|_ a by A3, Def1;

      then ((c + ( - (( ProJ (a,(b + p),c)) * b))) + (( - (( ProJ (a,(b + p),c)) * p)) + (( ProJ (a,(b + p),c)) * p))) _|_ a by RLVECT_1:def 3;

      then ((c + ( - (( ProJ (a,(b + p),c)) * b))) + 0V) _|_ a by RLVECT_1: 5;

      then

       A5: (c - (( ProJ (a,(b + p),c)) * b)) _|_ a by RLVECT_1: 4;

      (c - (( ProJ (a,b,c)) * b)) _|_ a by A1, Th14;

      hence thesis by A1, A5, A4, Th12;

    end;

    theorem :: SYMSP_1:20

    

     Th20: not b _|_ a & p _|_ b & p _|_ c implies ( ProJ ((a + p),b,c)) = ( ProJ (a,b,c))

    proof

      assume that

       A1: not b _|_ a and

       A2: p _|_ b and

       A3: p _|_ c;

      b _|_ p by A2, Th2;

      then (( ProJ (a,b,c)) * b) _|_ p by Def1;

      then

       A4: ( - (( ProJ (a,b,c)) * b)) _|_ p by Th6;

      c _|_ p by A3, Th2;

      then (c + ( - (( ProJ (a,b,c)) * b))) _|_ p by A4, Def1;

      then

       A5: p _|_ (c - (( ProJ (a,b,c)) * b)) by Th2;

      (c - (( ProJ (a,b,c)) * b)) _|_ a by A1, Th14;

      then a _|_ (c - (( ProJ (a,b,c)) * b)) by Th2;

      then (a + p) _|_ (c - (( ProJ (a,b,c)) * b)) by A5, Def1;

      then

       A6: (c - (( ProJ (a,b,c)) * b)) _|_ (a + p) by Th2;

       not a _|_ b by A1, Th2;

      then not (a + p) _|_ b by A2, Th4;

      then

       A7: not b _|_ (a + p) by Th2;

      then (c - (( ProJ ((a + p),b,c)) * b)) _|_ (a + p) by Th14;

      hence thesis by A7, A6, Th12;

    end;

    theorem :: SYMSP_1:21

    

     Th21: not b _|_ a & (c - b) _|_ a implies ( ProJ (a,b,c)) = ( 1_ F)

    proof

      assume that

       A1: not b _|_ a and

       A2: (c - b) _|_ a;

      (c - (( 1_ F) * b)) _|_ a & (c - (( ProJ (a,b,c)) * b)) _|_ a by A1, A2, Th14, VECTSP_1:def 17;

      hence thesis by A1, Th12;

    end;

    theorem :: SYMSP_1:22

    

     Th22: not b _|_ a implies ( ProJ (a,b,b)) = ( 1_ F)

    proof

      

       A1: (b - b) = ( 0. S) by RLVECT_1: 5;

      assume not b _|_ a;

      hence thesis by A1, Th1, Th21;

    end;

    theorem :: SYMSP_1:23

    

     Th23: not b _|_ a implies (x _|_ a iff ( ProJ (a,b,x)) = ( 0. F))

    proof

      set 0F = ( 0. F), 0V = ( 0. S);

       A1:

      now

        assume that

         A2: not b _|_ a and

         A3: x _|_ a;

        (x + 0V) _|_ a by A3, RLVECT_1: 4;

        then (x + ( - 0V)) _|_ a by RLVECT_1: 12;

        then

         A4: (x - (0F * b)) _|_ a by VECTSP_1: 14;

        (x - (( ProJ (a,b,x)) * b)) _|_ a by A2, Th14;

        hence ( ProJ (a,b,x)) = ( 0. F) by A2, A4, Th12;

      end;

      now

        assume ( not b _|_ a) & ( ProJ (a,b,x)) = ( 0. F);

        then (x - (0F * b)) _|_ a by Th14;

        then (x - 0V) _|_ a by VECTSP_1: 14;

        then (x + 0V) _|_ a by RLVECT_1: 12;

        hence x _|_ a by RLVECT_1: 4;

      end;

      hence thesis by A1;

    end;

    theorem :: SYMSP_1:24

    

     Th24: not b _|_ a & not q _|_ a implies (( ProJ (a,b,p)) * (( ProJ (a,b,q)) " )) = ( ProJ (a,q,p))

    proof

      assume that

       A1: not b _|_ a and

       A2: not q _|_ a;

      ((( ProJ (a,q,p)) * q) - (( ProJ (a,b,(( ProJ (a,q,p)) * q))) * b)) _|_ a & (p - (( ProJ (a,q,p)) * q)) _|_ a by A1, A2, Th14;

      then ((p + ( - (( ProJ (a,q,p)) * q))) + ((( ProJ (a,q,p)) * q) - (( ProJ (a,b,(( ProJ (a,q,p)) * q))) * b))) _|_ a by Def1;

      then (((p + ( - (( ProJ (a,q,p)) * q))) + (( ProJ (a,q,p)) * q)) + ( - (( ProJ (a,b,(( ProJ (a,q,p)) * q))) * b))) _|_ a by RLVECT_1:def 3;

      then ((p + (( - (( ProJ (a,q,p)) * q)) + (( ProJ (a,q,p)) * q))) + ( - (( ProJ (a,b,(( ProJ (a,q,p)) * q))) * b))) _|_ a by RLVECT_1:def 3;

      then ((p + ( 0. S)) + ( - (( ProJ (a,b,(( ProJ (a,q,p)) * q))) * b))) _|_ a by RLVECT_1: 5;

      then (p + ( - (( ProJ (a,b,(( ProJ (a,q,p)) * q))) * b))) _|_ a by RLVECT_1: 4;

      then

       A3: (p - ((( ProJ (a,q,p)) * ( ProJ (a,b,q))) * b)) _|_ a by A1, Th15;

      (p - (( ProJ (a,b,p)) * b)) _|_ a by A1, Th14;

      then (( ProJ (a,q,p)) * ( ProJ (a,b,q))) = ( ProJ (a,b,p)) by A1, A3, Th12;

      then

       A4: (( ProJ (a,q,p)) * (( ProJ (a,b,q)) * (( ProJ (a,b,q)) " ))) = (( ProJ (a,b,p)) * (( ProJ (a,b,q)) " )) by GROUP_1:def 3;

      ( ProJ (a,b,q)) <> ( 0. F) by A1, A2, Th23;

      then (( ProJ (a,q,p)) * ( 1_ F)) = (( ProJ (a,b,p)) * (( ProJ (a,b,q)) " )) by A4, VECTSP_1:def 10;

      hence thesis;

    end;

    theorem :: SYMSP_1:25

    

     Th25: not b _|_ a & not c _|_ a implies ( ProJ (a,b,c)) = (( ProJ (a,c,b)) " )

    proof

      set 1F = ( 1_ F), 0F = ( 0. F);

      assume that

       A1: not b _|_ a and

       A2: not c _|_ a;

      

       A3: ( ProJ (a,c,b)) <> 0F by A1, A2, Th23;

      (( ProJ (a,b,b)) * (( ProJ (a,b,c)) " )) = ( ProJ (a,c,b)) by A1, A2, Th24;

      then ((( ProJ (a,b,c)) " ) * 1F) = ( ProJ (a,c,b)) by A1, Th22;

      then

       A4: (( ProJ (a,b,c)) " ) = ( ProJ (a,c,b));

      ( ProJ (a,b,c)) <> 0F by A1, A2, Th23;

      then 1F = (( ProJ (a,c,b)) * ( ProJ (a,b,c))) by A4, VECTSP_1:def 10;

      

      then (( ProJ (a,c,b)) " ) = ((( ProJ (a,c,b)) " ) * (( ProJ (a,c,b)) * ( ProJ (a,b,c))))

      .= (((( ProJ (a,c,b)) " ) * ( ProJ (a,c,b))) * ( ProJ (a,b,c))) by GROUP_1:def 3

      .= (( ProJ (a,b,c)) * 1F) by A3, VECTSP_1:def 10;

      hence thesis;

    end;

    theorem :: SYMSP_1:26

    

     Th26: not b _|_ a & b _|_ (c + a) implies ( ProJ (a,b,c)) = ( ProJ (c,b,a))

    proof

      assume that

       A1: not b _|_ a and

       A2: b _|_ (c + a);

      (( ProJ (a,b,c)) * b) _|_ (c + a) by A2, Def1;

      then

       A3: ( - (( ProJ (a,b,c)) * b)) _|_ (c + a) by Th6;

      (c - (( ProJ (a,b,c)) * b)) _|_ a by A1, Th14;

      then a _|_ (( - (( ProJ (a,b,c)) * b)) + c) by Th2;

      then c _|_ (a + ( - (( ProJ (a,b,c)) * b))) by A3, Def1;

      then

       A4: (a - (( ProJ (a,b,c)) * b)) _|_ c by Th2;

      ( not a _|_ b) & (c + a) _|_ b by A1, A2, Th2;

      then not c _|_ b by Th3;

      then

       A5: not b _|_ c by Th2;

      then (a - (( ProJ (c,b,a)) * b)) _|_ c by Th14;

      hence thesis by A5, A4, Th12;

    end;

    theorem :: SYMSP_1:27

    

     Th27: not a _|_ b & not c _|_ b implies ( ProJ (c,b,a)) = (( - (( ProJ (b,a,c)) " )) * ( ProJ (a,b,c)))

    proof

      set 1F = ( 1_ F);

      assume that

       A1: not a _|_ b and

       A2: not c _|_ b;

      

       A3: ( ProJ (b,a,c)) <> ( 0. F) by A1, A2, Th23;

      then

       A4: ( - (( ProJ (b,a,c)) " )) <> ( 0. F) by VECTSP_1: 25;

      (( - 1F) * ((( ProJ (b,a,c)) " ) * ( ProJ (b,a,c)))) = (( - 1F) * 1F) by A3, VECTSP_1:def 10;

      then ((( - 1F) * (( ProJ (b,a,c)) " )) * ( ProJ (b,a,c))) = (( - 1F) * 1F) by GROUP_1:def 3;

      then ((( - 1F) * (( ProJ (b,a,c)) " )) * ( ProJ (b,a,c))) = ( - 1F);

      then (( - ((( ProJ (b,a,c)) " ) * 1F)) * ( ProJ (b,a,c))) = ( - 1F) by VECTSP_1: 9;

      then (( - (( ProJ (b,a,c)) " )) * ( ProJ (b,a,c))) = ( - 1F);

      then ( ProJ (b,a,(( - (( ProJ (b,a,c)) " )) * c))) = ( - 1F) by A1, Th15;

      then ((( - (( ProJ (b,a,c)) " )) * c) - (( - 1F) * a)) _|_ b by A1, Th14;

      then ((( - (( ProJ (b,a,c)) " )) * c) - ( - a)) _|_ b by VECTSP_1: 14;

      then ((( - (( ProJ (b,a,c)) " )) * c) + a) _|_ b by RLVECT_1: 17;

      then

       A5: b _|_ ((( - (( ProJ (b,a,c)) " )) * c) + a) by Th2;

       not b _|_ a by A1, Th2;

      then ( ProJ (a,b,(( - (( ProJ (b,a,c)) " )) * c))) = ( ProJ ((( - (( ProJ (b,a,c)) " )) * c),b,a)) by A5, Th26;

      then ( ProJ (a,b,(( - (( ProJ (b,a,c)) " )) * c))) = ( ProJ (c,b,a)) by A2, A4, Th2, Th18;

      hence thesis by A1, Th2, Th15;

    end;

    theorem :: SYMSP_1:28

    

     Th28: (( 1_ F) + ( 1_ F)) <> ( 0. F) & not a _|_ p & not a _|_ q & not b _|_ q implies (( ProJ (a,p,q)) * ( ProJ (b,q,p))) = (( ProJ (p,a,b)) * ( ProJ (q,b,a)))

    proof

      assume that

       A1: (( 1_ F) + ( 1_ F)) <> ( 0. F) and

       A2: not a _|_ p and

       A3: not a _|_ q and

       A4: not b _|_ q;

       A5:

      now

        assume that

         A6: p _|_ q and

         A7: a _|_ b;

         not q _|_ b by A4, Th2;

        then

         A8: ( ProJ (b,q,p)) = ( ProJ (b,q,(p + a))) by A7, Th19;

        

         A9: not (p + a) _|_ q by A3, A6, Th4;

        then

         A10: ( ProJ (b,q,(p + a))) = (( - (( ProJ (q,(p + a),b)) " )) * ( ProJ ((p + a),q,b))) by A4, Th27;

        

         A11: a _|_ a by A1, Th13;

        

         A12: not p _|_ a by A2, Th2;

        then

         A13: ( ProJ (a,p,q)) = ( ProJ (a,(p + a),q)) by A11, Th19;

         not (p + a) _|_ a by A12, A11, Th4;

        then

         A14: not a _|_ (p + a) by Th2;

        

         A15: not q _|_ (p + a) by A9, Th2;

        then ( ProJ (a,(p + a),q)) = (( - (( ProJ ((p + a),q,a)) " )) * ( ProJ (q,(p + a),a))) by A14, Th27;

        

        then (( ProJ (a,p,q)) * ( ProJ (b,q,p))) = (((( ProJ (q,(p + a),a)) * ( - (( ProJ ((p + a),q,a)) " ))) * ( - (( ProJ (q,(p + a),b)) " ))) * ( ProJ ((p + a),q,b))) by A13, A8, A10, GROUP_1:def 3

        .= ((( ProJ (q,(p + a),a)) * (( - (( ProJ ((p + a),q,a)) " )) * ( - (( ProJ (q,(p + a),b)) " )))) * ( ProJ ((p + a),q,b))) by GROUP_1:def 3

        .= ((( ProJ (q,(p + a),a)) * ((( ProJ (q,(p + a),b)) " ) * (( ProJ ((p + a),q,a)) " ))) * ( ProJ ((p + a),q,b))) by VECTSP_1: 10

        .= (((( ProJ (q,(p + a),a)) * (( ProJ (q,(p + a),b)) " )) * (( ProJ ((p + a),q,a)) " )) * ( ProJ ((p + a),q,b))) by GROUP_1:def 3

        .= ((( ProJ (q,b,a)) * (( ProJ ((p + a),q,a)) " )) * ( ProJ ((p + a),q,b))) by A4, A9, Th24

        .= (( ProJ (q,b,a)) * (( ProJ ((p + a),q,b)) * (( ProJ ((p + a),q,a)) " ))) by GROUP_1:def 3

        .= (( ProJ (q,b,a)) * ( ProJ ((p + a),a,b))) by A14, A15, Th24

        .= (( ProJ (q,b,a)) * ( ProJ (p,a,b))) by A2, A7, A11, Th20;

        hence thesis;

      end;

       A16:

      now

        assume

         A17: not a _|_ b;

        

         A18: not q _|_ b by A4, Th2;

        then

         A19: ( ProJ (q,b,a)) = (( - (( ProJ (b,a,q)) " )) * ( ProJ (a,b,q))) by A17, Th27;

        

         A20: not p _|_ a by A2, Th2;

        

         A21: not b _|_ a by A17, Th2;

        then ( ProJ (p,a,b)) = (( - (( ProJ (a,b,p)) " )) * ( ProJ (b,a,p))) by A20, Th27;

        

        then (( ProJ (p,a,b)) * ( ProJ (q,b,a))) = (((( ProJ (b,a,p)) * ( - (( ProJ (a,b,p)) " ))) * ( - (( ProJ (b,a,q)) " ))) * ( ProJ (a,b,q))) by A19, GROUP_1:def 3

        .= ((( ProJ (b,a,p)) * (( - (( ProJ (a,b,p)) " )) * ( - (( ProJ (b,a,q)) " )))) * ( ProJ (a,b,q))) by GROUP_1:def 3

        .= ((( ProJ (b,a,p)) * ((( ProJ (b,a,q)) " ) * (( ProJ (a,b,p)) " ))) * ( ProJ (a,b,q))) by VECTSP_1: 10

        .= (((( ProJ (b,a,p)) * (( ProJ (b,a,q)) " )) * (( ProJ (a,b,p)) " )) * ( ProJ (a,b,q))) by GROUP_1:def 3

        .= ((( ProJ (b,q,p)) * (( ProJ (a,b,p)) " )) * ( ProJ (a,b,q))) by A17, A18, Th24

        .= (( ProJ (b,q,p)) * (( ProJ (a,b,q)) * (( ProJ (a,b,p)) " ))) by GROUP_1:def 3

        .= (( ProJ (b,q,p)) * ( ProJ (a,p,q))) by A21, A20, Th24;

        hence thesis;

      end;

      now

        assume

         A22: not p _|_ q;

        then

         A23: ( ProJ (b,q,p)) = (( - (( ProJ (q,p,b)) " )) * ( ProJ (p,q,b))) by A4, Th27;

        

         A24: not q _|_ p by A22, Th2;

        then ( ProJ (a,p,q)) = (( - (( ProJ (p,q,a)) " )) * ( ProJ (q,p,a))) by A2, Th27;

        

        then (( ProJ (a,p,q)) * ( ProJ (b,q,p))) = (((( ProJ (q,p,a)) * ( - (( ProJ (p,q,a)) " ))) * ( - (( ProJ (q,p,b)) " ))) * ( ProJ (p,q,b))) by A23, GROUP_1:def 3

        .= ((( ProJ (q,p,a)) * (( - (( ProJ (p,q,a)) " )) * ( - (( ProJ (q,p,b)) " )))) * ( ProJ (p,q,b))) by GROUP_1:def 3

        .= ((( ProJ (q,p,a)) * ((( ProJ (q,p,b)) " ) * (( ProJ (p,q,a)) " ))) * ( ProJ (p,q,b))) by VECTSP_1: 10

        .= (((( ProJ (q,p,a)) * (( ProJ (q,p,b)) " )) * (( ProJ (p,q,a)) " )) * ( ProJ (p,q,b))) by GROUP_1:def 3

        .= ((( ProJ (q,b,a)) * (( ProJ (p,q,a)) " )) * ( ProJ (p,q,b))) by A4, A22, Th24

        .= (( ProJ (q,b,a)) * (( ProJ (p,q,b)) * (( ProJ (p,q,a)) " ))) by GROUP_1:def 3

        .= (( ProJ (q,b,a)) * ( ProJ (p,a,b))) by A2, A24, Th24;

        hence thesis;

      end;

      hence thesis by A16, A5;

    end;

    theorem :: SYMSP_1:29

    

     Th29: (( 1_ F) + ( 1_ F)) <> ( 0. F) & not p _|_ a & not p _|_ x & not q _|_ a & not q _|_ x implies (( ProJ (a,q,p)) * ( ProJ (p,a,x))) = (( ProJ (x,q,p)) * ( ProJ (q,a,x)))

    proof

      set 0F = ( 0. F), 1F = ( 1_ F);

      assume that

       A1: (( 1_ F) + ( 1_ F)) <> ( 0. F) and

       A2: not p _|_ a and

       A3: not p _|_ x and

       A4: not q _|_ a and

       A5: not q _|_ x;

      

       A6: ( not a _|_ q) & not x _|_ q by A4, A5, Th2;

      (( ProJ (p,a,x)) * ( ProJ (q,x,a))) = (( ProJ (a,p,q)) * ( ProJ (x,q,p))) by A1, A2, A3, A5, Th28;

      then (( ProJ (p,a,x)) * ( ProJ (q,x,a))) = ((( ProJ (a,q,p)) " ) * ( ProJ (x,q,p))) by A2, A4, Th25;

      then

       A7: (( ProJ (a,q,p)) * (( ProJ (p,a,x)) * ( ProJ (q,x,a)))) = ((( ProJ (a,q,p)) * (( ProJ (a,q,p)) " )) * ( ProJ (x,q,p))) by GROUP_1:def 3;

      ( ProJ (a,q,p)) <> 0F by A2, A4, Th23;

      then (( ProJ (a,q,p)) * (( ProJ (p,a,x)) * ( ProJ (q,x,a)))) = (( ProJ (x,q,p)) * 1F) by A7, VECTSP_1:def 10;

      then (( ProJ (a,q,p)) * (( ProJ (p,a,x)) * ( ProJ (q,x,a)))) = ( ProJ (x,q,p));

      then ((( ProJ (a,q,p)) * ( ProJ (p,a,x))) * ( ProJ (q,x,a))) = ( ProJ (x,q,p)) by GROUP_1:def 3;

      then ((( ProJ (a,q,p)) * ( ProJ (p,a,x))) * (( ProJ (q,a,x)) " )) = ( ProJ (x,q,p)) by A6, Th25;

      then

       A8: ((( ProJ (a,q,p)) * ( ProJ (p,a,x))) * ((( ProJ (q,a,x)) " ) * ( ProJ (q,a,x)))) = (( ProJ (x,q,p)) * ( ProJ (q,a,x))) by GROUP_1:def 3;

      ( ProJ (q,a,x)) <> 0F by A6, Th23;

      then ((( ProJ (a,q,p)) * ( ProJ (p,a,x))) * 1F) = (( ProJ (x,q,p)) * ( ProJ (q,a,x))) by A8, VECTSP_1:def 10;

      hence thesis;

    end;

    theorem :: SYMSP_1:30

    

     Th30: (( 1_ F) + ( 1_ F)) <> ( 0. F) & not p _|_ a & not p _|_ x & not q _|_ a & not q _|_ x & not b _|_ a implies ((( ProJ (a,b,p)) * ( ProJ (p,a,x))) * ( ProJ (x,p,y))) = ((( ProJ (a,b,q)) * ( ProJ (q,a,x))) * ( ProJ (x,q,y)))

    proof

      set 0F = ( 0. F), 1F = ( 1_ F);

      assume that

       A1: (( 1_ F) + ( 1_ F)) <> ( 0. F) & not p _|_ a and

       A2: not p _|_ x and

       A3: not q _|_ a and

       A4: not q _|_ x and

       A5: not b _|_ a;

       A6:

      now

        

         A7: ( ProJ (a,b,q)) <> 0F by A3, A5, Th23;

        assume

         A8: not y _|_ x;

        (( ProJ (a,q,p)) * ( ProJ (p,a,x))) = (( ProJ (x,q,p)) * ( ProJ (q,a,x))) by A1, A2, A3, A4, Th29;

        then ((( ProJ (a,b,p)) * (( ProJ (a,b,q)) " )) * ( ProJ (p,a,x))) = (( ProJ (x,q,p)) * ( ProJ (q,a,x))) by A3, A5, Th24;

        then (((( ProJ (a,b,q)) " ) * ( ProJ (a,b,p))) * ( ProJ (p,a,x))) = ((( ProJ (x,y,p)) * (( ProJ (x,y,q)) " )) * ( ProJ (q,a,x))) by A4, A8, Th24;

        then (( ProJ (a,b,q)) * ((( ProJ (a,b,q)) " ) * (( ProJ (a,b,p)) * ( ProJ (p,a,x))))) = (( ProJ (a,b,q)) * ((( ProJ (x,y,p)) * (( ProJ (x,y,q)) " )) * ( ProJ (q,a,x)))) by GROUP_1:def 3;

        then ((( ProJ (a,b,q)) * (( ProJ (a,b,q)) " )) * (( ProJ (a,b,p)) * ( ProJ (p,a,x)))) = (( ProJ (a,b,q)) * ((( ProJ (x,y,p)) * (( ProJ (x,y,q)) " )) * ( ProJ (q,a,x)))) by GROUP_1:def 3;

        then ((( ProJ (a,b,p)) * ( ProJ (p,a,x))) * 1F) = (( ProJ (a,b,q)) * ((( ProJ (x,y,p)) * (( ProJ (x,y,q)) " )) * ( ProJ (q,a,x)))) by A7, VECTSP_1:def 10;

        then (( ProJ (a,b,p)) * ( ProJ (p,a,x))) = (( ProJ (a,b,q)) * ((( ProJ (x,y,p)) * (( ProJ (x,y,q)) " )) * ( ProJ (q,a,x))));

        then (( ProJ (a,b,p)) * ( ProJ (p,a,x))) = (( ProJ (a,b,q)) * (((( ProJ (x,y,q)) " ) * (( ProJ (x,p,y)) " )) * ( ProJ (q,a,x)))) by A2, A8, Th25;

        then (( ProJ (a,b,p)) * ( ProJ (p,a,x))) = ((( ProJ (a,b,q)) * ((( ProJ (x,y,q)) " ) * (( ProJ (x,p,y)) " ))) * ( ProJ (q,a,x))) by GROUP_1:def 3;

        then (( ProJ (a,b,p)) * ( ProJ (p,a,x))) = (( ProJ (q,a,x)) * ((( ProJ (a,b,q)) * (( ProJ (x,y,q)) " )) * (( ProJ (x,p,y)) " ))) by GROUP_1:def 3;

        then ((( ProJ (a,b,p)) * ( ProJ (p,a,x))) * ( ProJ (x,p,y))) = (((( ProJ (q,a,x)) * (( ProJ (a,b,q)) * (( ProJ (x,y,q)) " ))) * (( ProJ (x,p,y)) " )) * ( ProJ (x,p,y))) by GROUP_1:def 3;

        then

         A9: ((( ProJ (a,b,p)) * ( ProJ (p,a,x))) * ( ProJ (x,p,y))) = ((( ProJ (q,a,x)) * (( ProJ (a,b,q)) * (( ProJ (x,y,q)) " ))) * ((( ProJ (x,p,y)) " ) * ( ProJ (x,p,y)))) by GROUP_1:def 3;

        ( ProJ (x,p,y)) <> 0F by A2, A8, Th23;

        then ((( ProJ (a,b,p)) * ( ProJ (p,a,x))) * ( ProJ (x,p,y))) = ((( ProJ (q,a,x)) * (( ProJ (a,b,q)) * (( ProJ (x,y,q)) " ))) * 1F) by A9, VECTSP_1:def 10;

        then ((( ProJ (a,b,p)) * ( ProJ (p,a,x))) * ( ProJ (x,p,y))) = (( ProJ (q,a,x)) * (( ProJ (a,b,q)) * (( ProJ (x,y,q)) " )));

        then ((( ProJ (a,b,p)) * ( ProJ (p,a,x))) * ( ProJ (x,p,y))) = (( ProJ (q,a,x)) * (( ProJ (a,b,q)) * ( ProJ (x,q,y)))) by A4, A8, Th25;

        hence thesis by GROUP_1:def 3;

      end;

      now

        assume

         A10: y _|_ x;

        then ( ProJ (x,p,y)) = 0F by A2, Th23;

        then

         A11: ((( ProJ (a,b,p)) * ( ProJ (p,a,x))) * ( ProJ (x,p,y))) = 0F;

        ( ProJ (x,q,y)) = 0F by A4, A10, Th23;

        hence thesis by A11;

      end;

      hence thesis by A6;

    end;

    theorem :: SYMSP_1:31

    

     Th31: not a _|_ p & not x _|_ p & not y _|_ p implies (( ProJ (p,a,x)) * ( ProJ (x,p,y))) = (( - ( ProJ (p,a,y))) * ( ProJ (y,p,x)))

    proof

      set 0F = ( 0. F), 1F = ( 1_ F);

      assume that

       A1: not a _|_ p and

       A2: not x _|_ p and

       A3: not y _|_ p;

      

       A4: not p _|_ y by A3, Th2;

      

       A5: not p _|_ x by A2, Th2;

       A6:

      now

        

         A7: ( ProJ (p,a,x)) <> 0F by A1, A2, Th23;

        assume

         A8: not y _|_ x;

        then

         A9: not x _|_ y by Th2;

        (( ProJ (p,a,y)) * (( ProJ (p,a,x)) " )) = ( ProJ (p,x,y)) by A1, A2, Th24;

        then ((( ProJ (p,a,y)) * (( ProJ (p,a,x)) " )) * ( ProJ (p,a,x))) = ((( - (( ProJ (x,y,p)) " )) * ( ProJ (y,x,p))) * ( ProJ (p,a,x))) by A5, A8, Th27;

        then (( ProJ (p,a,y)) * ((( ProJ (p,a,x)) " ) * ( ProJ (p,a,x)))) = ((( - (( ProJ (x,y,p)) " )) * ( ProJ (y,x,p))) * ( ProJ (p,a,x))) by GROUP_1:def 3;

        then (( ProJ (p,a,y)) * 1F) = ((( - (( ProJ (x,y,p)) " )) * ( ProJ (y,x,p))) * ( ProJ (p,a,x))) by A7, VECTSP_1:def 10;

        then ( ProJ (p,a,y)) = ((( ProJ (y,x,p)) * ( - (( ProJ (x,y,p)) " ))) * ( ProJ (p,a,x)));

        then ( ProJ (p,a,y)) = (( ProJ (y,x,p)) * (( - (( ProJ (x,y,p)) " )) * ( ProJ (p,a,x)))) by GROUP_1:def 3;

        then (( ProJ (y,p,x)) * ( ProJ (p,a,y))) = (( ProJ (y,p,x)) * ((( ProJ (y,p,x)) " ) * (( - (( ProJ (x,y,p)) " )) * ( ProJ (p,a,x))))) by A4, A9, Th25;

        then

         A10: (( ProJ (y,p,x)) * ( ProJ (p,a,y))) = ((( ProJ (y,p,x)) * (( ProJ (y,p,x)) " )) * (( - (( ProJ (x,y,p)) " )) * ( ProJ (p,a,x)))) by GROUP_1:def 3;

        ( ProJ (y,p,x)) <> 0F by A4, A9, Th23;

        then (( ProJ (y,p,x)) * ( ProJ (p,a,y))) = ((( - (( ProJ (x,y,p)) " )) * ( ProJ (p,a,x))) * 1F) by A10, VECTSP_1:def 10;

        then (( ProJ (p,a,y)) * ( ProJ (y,p,x))) = (( - (( ProJ (x,y,p)) " )) * ( ProJ (p,a,x)));

        then ( - (( ProJ (p,a,y)) * ( ProJ (y,p,x)))) = ( - ( - ((( ProJ (x,y,p)) " ) * ( ProJ (p,a,x))))) by VECTSP_1: 9;

        then ( - (( ProJ (p,a,y)) * ( ProJ (y,p,x)))) = ((( ProJ (x,y,p)) " ) * ( ProJ (p,a,x))) by RLVECT_1: 17;

        then (( - ( ProJ (p,a,y))) * ( ProJ (y,p,x))) = ((( ProJ (x,y,p)) " ) * ( ProJ (p,a,x))) by VECTSP_1: 9;

        hence thesis by A5, A8, Th25;

      end;

      now

        assume

         A11: y _|_ x;

        then ( ProJ (x,p,y)) = 0F by A5, Th23;

        then

         A12: (( ProJ (p,a,x)) * ( ProJ (x,p,y))) = 0F;

        x _|_ y by A11, Th2;

        then ( ProJ (y,p,x)) = 0F by A4, Th23;

        hence thesis by A12;

      end;

      hence thesis by A6;

    end;

    definition

      let F, S, x, y, a, b;

      assume

       A1: ( not b _|_ a) & (( 1_ F) + ( 1_ F)) <> ( 0. F);

      :: SYMSP_1:def3

      func PProJ (a,b,x,y) -> Element of F means

      : Def3: for q st not q _|_ a & not q _|_ x holds it = ((( ProJ (a,b,q)) * ( ProJ (q,a,x))) * ( ProJ (x,q,y))) if ex p st not p _|_ a & not p _|_ x

      otherwise it = ( 0. F);

      existence

      proof

        thus (ex p st not p _|_ a & not p _|_ x) implies ex IT be Element of F st for q st not q _|_ a & not q _|_ x holds IT = ((( ProJ (a,b,q)) * ( ProJ (q,a,x))) * ( ProJ (x,q,y)))

        proof

          given p such that

           A2: ( not p _|_ a) & not p _|_ x;

          take ((( ProJ (a,b,p)) * ( ProJ (p,a,x))) * ( ProJ (x,p,y)));

          let q;

          assume ( not q _|_ a) & not q _|_ x;

          hence thesis by A1, A2, Th30;

        end;

        thus thesis;

      end;

      uniqueness

      proof

        let IT1,IT2 be Element of F;

        thus (ex p st not p _|_ a & not p _|_ x) & (for q st not q _|_ a & not q _|_ x holds IT1 = ((( ProJ (a,b,q)) * ( ProJ (q,a,x))) * ( ProJ (x,q,y)))) & (for q st not q _|_ a & not q _|_ x holds IT2 = ((( ProJ (a,b,q)) * ( ProJ (q,a,x))) * ( ProJ (x,q,y)))) implies IT1 = IT2

        proof

          given p such that

           A3: ( not p _|_ a) & not p _|_ x;

          consider r such that

           A4: ( not r _|_ a) & not r _|_ x by A3;

          assume that

           A5: for q st not q _|_ a & not q _|_ x holds IT1 = ((( ProJ (a,b,q)) * ( ProJ (q,a,x))) * ( ProJ (x,q,y))) and

           A6: for q st not q _|_ a & not q _|_ x holds IT2 = ((( ProJ (a,b,q)) * ( ProJ (q,a,x))) * ( ProJ (x,q,y)));

          IT1 = ((( ProJ (a,b,r)) * ( ProJ (r,a,x))) * ( ProJ (x,r,y))) by A5, A4;

          hence thesis by A6, A4;

        end;

        thus thesis;

      end;

      consistency ;

    end

    theorem :: SYMSP_1:32

    

     Th32: (( 1_ F) + ( 1_ F)) <> ( 0. F) & not b _|_ a & x = ( 0. S) implies ( PProJ (a,b,x,y)) = ( 0. F)

    proof

      assume that

       A1: (( 1_ F) + ( 1_ F)) <> ( 0. F) & not b _|_ a and

       A2: x = ( 0. S);

      for p holds p _|_ a or p _|_ x by A2, Th1, Th2;

      hence thesis by A1, Def3;

    end;

    theorem :: SYMSP_1:33

    

     Th33: (( 1_ F) + ( 1_ F)) <> ( 0. F) & not b _|_ a implies (( PProJ (a,b,x,y)) = ( 0. F) iff y _|_ x)

    proof

      set 0F = ( 0. F);

      assume that

       A1: (( 1_ F) + ( 1_ F)) <> ( 0. F) and

       A2: not b _|_ a;

      

       A3: a <> ( 0. S) by A2, Th1, Th2;

      

       A4: ( PProJ (a,b,x,y)) = ( 0. F) implies y _|_ x

      proof

        assume

         A5: ( PProJ (a,b,x,y)) = ( 0. F);

         A6:

        now

          given p such that

           A7: not p _|_ a and

           A8: not p _|_ x;

           A9:

          now

            assume

             A10: ( ProJ (p,a,x)) = ( 0. F);

             not a _|_ p by A7, Th2;

            then x _|_ p by A10, Th23;

            hence contradiction by A8, Th2;

          end;

          ((( ProJ (a,b,p)) * ( ProJ (p,a,x))) * ( ProJ (x,p,y))) = 0F by A1, A2, A5, A7, A8, Def3;

          then (( ProJ (a,b,p)) * ( ProJ (p,a,x))) = 0F or ( ProJ (x,p,y)) = 0F by VECTSP_1: 12;

          then ( ProJ (a,b,p)) = ( 0. F) or ( ProJ (p,a,x)) = ( 0. F) or ( ProJ (x,p,y)) = ( 0. F) by VECTSP_1: 12;

          hence thesis by A2, A7, A8, A9, Th23;

        end;

        now

          assume for p holds p _|_ a or p _|_ x;

          then x = ( 0. S) by A3, Th9;

          hence thesis by Th1, Th2;

        end;

        hence thesis by A6;

      end;

      y _|_ x implies ( PProJ (a,b,x,y)) = ( 0. F)

      proof

        assume

         A11: y _|_ x;

         A12:

        now

          assume x <> ( 0. S);

          then

          consider p such that

           A13: not p _|_ a and

           A14: not p _|_ x by A3, Th9;

          ( ProJ (x,p,y)) = 0F by A11, A14, Th23;

          then ((( ProJ (a,b,p)) * ( ProJ (p,a,x))) * ( ProJ (x,p,y))) = ( 0. F);

          hence thesis by A1, A2, A13, A14, Def3;

        end;

        now

          assume x = ( 0. S);

          then for p holds p _|_ a or p _|_ x by Th1, Th2;

          hence thesis by A1, A2, Def3;

        end;

        hence thesis by A12;

      end;

      hence thesis by A4;

    end;

    theorem :: SYMSP_1:34

    (( 1_ F) + ( 1_ F)) <> ( 0. F) & not b _|_ a implies ( PProJ (a,b,x,y)) = ( - ( PProJ (a,b,y,x)))

    proof

      set 0F = ( 0. F), 1F = ( 1_ F);

      assume that

       A1: (( 1_ F) + ( 1_ F)) <> ( 0. F) and

       A2: not b _|_ a;

       A3:

      now

        assume not x _|_ y;

        then

         A4: x <> ( 0. S) & y <> ( 0. S) by Th1, Th2;

        a <> ( 0. S) by A2, Th1, Th2;

        then

        consider r such that

         A5: not r _|_ a and

         A6: not r _|_ x and

         A7: not r _|_ y by A1, A4, Th10;

        

         A8: not y _|_ r by A7, Th2;

        ( PProJ (a,b,y,x)) = ((( ProJ (a,b,r)) * ( ProJ (r,a,y))) * ( ProJ (y,r,x))) by A1, A2, A5, A7, Def3;

        then

         A9: ( PProJ (a,b,y,x)) = (( ProJ (a,b,r)) * (( ProJ (r,a,y)) * ( ProJ (y,r,x)))) by GROUP_1:def 3;

        ( not a _|_ r) & not x _|_ r by A5, A6, Th2;

        then ( PProJ (a,b,y,x)) = (( ProJ (a,b,r)) * (( - ( ProJ (r,a,x))) * ( ProJ (x,r,y)))) by A8, A9, Th31;

        then ( PProJ (a,b,y,x)) = ((( - ( ProJ (r,a,x))) * ( ProJ (a,b,r))) * ( ProJ (x,r,y))) by GROUP_1:def 3;

        then ( PProJ (a,b,y,x)) = (( - (( ProJ (r,a,x)) * ( ProJ (a,b,r)))) * ( ProJ (x,r,y))) by VECTSP_1: 9;

        then (( - 1F) * ( PProJ (a,b,y,x))) = (( - 1F) * ( - ((( ProJ (a,b,r)) * ( ProJ (r,a,x))) * ( ProJ (x,r,y))))) by VECTSP_1: 9;

        then ( - (( PProJ (a,b,y,x)) * 1F)) = (( - 1F) * ( - ((( ProJ (a,b,r)) * ( ProJ (r,a,x))) * ( ProJ (x,r,y))))) by VECTSP_1: 9;

        then ( - ( PProJ (a,b,y,x))) = (( - 1F) * ( - ((( ProJ (a,b,r)) * ( ProJ (r,a,x))) * ( ProJ (x,r,y)))));

        then

         A10: ( - ( PProJ (a,b,y,x))) = (((( ProJ (a,b,r)) * ( ProJ (r,a,x))) * ( ProJ (x,r,y))) * 1F) by VECTSP_1: 10;

        ( PProJ (a,b,x,y)) = ((( ProJ (a,b,r)) * ( ProJ (r,a,x))) * ( ProJ (x,r,y))) by A1, A2, A5, A6, Def3;

        hence thesis by A10;

      end;

      now

        assume

         A11: x _|_ y;

        then (( - 1F) * ( PProJ (a,b,y,x))) = (( - 1F) * 0F) by A1, A2, Th33;

        then ( - (( PProJ (a,b,y,x)) * 1F)) = (( - 1F) * 0F) by VECTSP_1: 9;

        then

         A12: ( - ( PProJ (a,b,y,x))) = (( - 1F) * 0F);

        y _|_ x by A11, Th2;

        then ( PProJ (a,b,x,y)) = 0F by A1, A2, Th33;

        hence thesis by A12;

      end;

      hence thesis by A3;

    end;

    theorem :: SYMSP_1:35

    (( 1_ F) + ( 1_ F)) <> ( 0. F) & not b _|_ a implies ( PProJ (a,b,x,(l * y))) = (l * ( PProJ (a,b,x,y)))

    proof

      set 0F = ( 0. F);

      assume that

       A1: (( 1_ F) + ( 1_ F)) <> ( 0. F) and

       A2: not b _|_ a;

       A3:

      now

        assume not x _|_ y;

        then

         A4: x <> ( 0. S) by Th1;

        a <> ( 0. S) by A2, Th1, Th2;

        then

        consider p such that

         A5: not p _|_ a and

         A6: not p _|_ x by A4, Th9;

        ( PProJ (a,b,x,(l * y))) = ((( ProJ (a,b,p)) * ( ProJ (p,a,x))) * ( ProJ (x,p,(l * y)))) by A1, A2, A5, A6, Def3;

        then

         A7: ( PProJ (a,b,x,(l * y))) = ((l * ( ProJ (x,p,y))) * (( ProJ (a,b,p)) * ( ProJ (p,a,x)))) by A6, Th15;

        ( PProJ (a,b,x,y)) = ((( ProJ (a,b,p)) * ( ProJ (p,a,x))) * ( ProJ (x,p,y))) by A1, A2, A5, A6, Def3;

        hence thesis by A7, GROUP_1:def 3;

      end;

      now

        assume

         A8: x _|_ y;

        then y _|_ x by Th2;

        then (l * y) _|_ x by Def1;

        then

         A9: ( PProJ (a,b,x,(l * y))) = 0F by A1, A2, Th33;

        y _|_ x by A8, Th2;

        then (l * ( PProJ (a,b,x,y))) = (l * 0F) by A1, A2, Th33;

        hence thesis by A9;

      end;

      hence thesis by A3;

    end;

    theorem :: SYMSP_1:36

    (( 1_ F) + ( 1_ F)) <> ( 0. F) & not b _|_ a implies ( PProJ (a,b,x,(y + z))) = (( PProJ (a,b,x,y)) + ( PProJ (a,b,x,z)))

    proof

      assume that

       A1: (( 1_ F) + ( 1_ F)) <> ( 0. F) and

       A2: not b _|_ a;

       A3:

      now

        assume

         A4: x <> ( 0. S);

        a <> ( 0. S) by A2, Th1, Th2;

        then

        consider p such that

         A5: ( not p _|_ a) & not p _|_ x by A4, Th9;

        

         A6: ( PProJ (a,b,x,(y + z))) = ((( ProJ (a,b,p)) * ( ProJ (p,a,x))) * ( ProJ (x,p,(y + z)))) & ( PProJ (a,b,x,y)) = ((( ProJ (a,b,p)) * ( ProJ (p,a,x))) * ( ProJ (x,p,y))) by A1, A2, A5, Def3;

        ( PProJ (a,b,x,z)) = ((( ProJ (a,b,p)) * ( ProJ (p,a,x))) * ( ProJ (x,p,z))) & ( ProJ (x,p,(y + z))) = (( ProJ (x,p,y)) + ( ProJ (x,p,z))) by A1, A2, A5, Def3, Th16;

        hence thesis by A6, VECTSP_1:def 7;

      end;

      set 0F = ( 0. F);

      now

        assume

         A7: x = ( 0. S);

        then

         A8: ( PProJ (a,b,x,z)) = 0F by A1, A2, Th32;

        ( PProJ (a,b,x,(y + z))) = 0F & ( PProJ (a,b,x,y)) = 0F by A1, A2, A7, Th32;

        hence thesis by A8, RLVECT_1: 4;

      end;

      hence thesis by A3;

    end;