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

A3: now :: thesis: ( not y _|_ implies PProJ (a,b,x,(l * y)) = l * (PProJ (a,b,x,y)) )

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

end;

now :: thesis: ( y _|_ implies PProJ (a,b,x,(l * y)) = l * (PProJ (a,b,x,y)) )

assume A8: y _|_ ; :: thesis: PProJ (a,b,x,(l * y)) = l * (PProJ (a,b,x,y))
then x _|_ by Th2;
then x _|_ by Def1;
then A9: PProJ (a,b,x,(l * y)) = 0. F by A1, A2, Th33;
x _|_ by A8, Th2;
then l * (PProJ (a,b,x,y)) = l * (0. F) by A1, A2, Th33;
hence PProJ (a,b,x,(l * y)) = l * (PProJ (a,b,x,y)) by A9; :: thesis: verum

end;

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