let F be Field; :: thesis: for S being OrtSp of F
for a, b, x, y, z being Element of S st not a _|_ holds
PProJ (a,b,x,(y + z)) = (PProJ (a,b,x,y)) + (PProJ (a,b,x,z))
let S be OrtSp of F; :: thesis: for a, b, x, y, z being Element of S st 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: ( not a _|_ implies PProJ (a,b,x,(y + z)) = (PProJ (a,b,x,y)) + (PProJ (a,b,x,z)) )
set 0F = 0. F;
assume A1: not a _|_ ; :: thesis: PProJ (a,b,x,(y + z)) = (PProJ (a,b,x,y)) + (PProJ (a,b,x,z))

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

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

end;

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

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

end;

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