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 ;
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 ; :: 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 ;
( 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 ; :: thesis: verum
end;
hence PProJ (a,b,x,(y + z)) = (PProJ (a,b,x,y)) + (PProJ (a,b,x,z)) by A2; :: thesis: verum