let F be Field; :: thesis: for S being SymSp of F
for a, b, x, y, z being Element of S st (1_ F) + (1_ F) <> 0. F & not a _|_ holds
PProJ (a,b,x,(y + z)) = (PProJ (a,b,x,y)) + (PProJ (a,b,x,z))
let S be SymSp of F; :: thesis: for a, b, x, y, z being Element of S st (1_ F) + (1_ F) <> 0. F & not a _|_ holds
PProJ (a,b,x,(y + z)) = (PProJ (a,b,x,y)) + (PProJ (a,b,x,z))
let a, b, x, y, z be Element of S; :: thesis: ( (1_ F) + (1_ F) <> 0. F & not a _|_ implies PProJ (a,b,x,(y + z)) = (PProJ (a,b,x,y)) + (PProJ (a,b,x,z)) )
assume that
A1: (1_ F) + (1_ F) <> 0. F and
A2: not a _|_ ; :: thesis: PProJ (a,b,x,(y + z)) = (PProJ (a,b,x,y)) + (PProJ (a,b,x,z))

A3: now :: thesis: ( x <> 0. S implies PProJ (a,b,x,(y + z)) = (PProJ (a,b,x,y)) + (PProJ (a,b,x,z)) )

assume A4: x <> 0. S ; :: thesis: PProJ (a,b,x,(y + z)) = (PProJ (a,b,x,y)) + (PProJ (a,b,x,z))
a <> 0. S by A2, Th1, Th2;
then consider p being Element of S such that
A5: ( not a _|_ & not 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 PProJ (a,b,x,(y + z)) = (PProJ (a,b,x,y)) + (PProJ (a,b,x,z)) by A6, VECTSP_1:def 7; :: thesis: verum

end;

set 0F = 0. F;

now :: thesis: ( x = 0. S implies PProJ (a,b,x,(y + z)) = (PProJ (a,b,x,y)) + (PProJ (a,b,x,z)) )

assume A7: x = 0. S ; :: thesis: PProJ (a,b,x,(y + z)) = (PProJ (a,b,x,y)) + (PProJ (a,b,x,z))
then A8: PProJ (a,b,x,z) = 0. F by A1, A2, Th32;
( PProJ (a,b,x,(y + z)) = 0. F & PProJ (a,b,x,y) = 0. F ) by A1, A2, A7, Th32;
hence PProJ (a,b,x,(y + z)) = (PProJ (a,b,x,y)) + (PProJ (a,b,x,z)) by A8, RLVECT_1:4; :: thesis: verum

end;

hence PProJ (a,b,x,(y + z)) = (PProJ (a,b,x,y)) + (PProJ (a,b,x,z)) by A3; :: thesis: verum