let F be Field; :: thesis: for S being SymSp of F
for b, a, 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 b, a, 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 b, a, 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

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, Th11, Th12;
then consider p being Element of S such that
A5: ( not a _|_ & not x _|_ ) by A4, Th21;
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, Def6;
( 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, Def6, Th29;
hence PProJ a,b,x,(y + z) = (PProJ a,b,x,y) + (PProJ a,b,x,z) by A6, VECTSP_1:def 18; :: thesis: verum

end;

set 0F = 0. F;

now

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, Th47;
( PProJ a,b,x,(y + z) = 0. F & PProJ a,b,x,y = 0. F ) by A1, A2, A7, Th47;
hence PProJ a,b,x,(y + z) = (PProJ a,b,x,y) + (PProJ a,b,x,z) by A8, RLVECT_1:10; :: thesis: verum

end;

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