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

assume not y _|_ ; :: thesis: PProJ a,b,x,(l * y) = l * (PProJ a,b,x,y)
then A4: x <> 0. S by Th11;
a <> 0. S by A2, Th11, Th12;
then consider p being Element of S such that
A5: not a _|_ and
A6: not x _|_ by A4, Th21;
PProJ a,b,x,(l * y) = ((ProJ a,b,p) * (ProJ p,a,x)) * (ProJ x,p,(l * y)) by A1, A2, A5, A6, Def6;
then A7: PProJ a,b,x,(l * y) = (l * (ProJ x,p,y)) * ((ProJ a,b,p) * (ProJ p,a,x)) by A6, Th28;
PProJ a,b,x,y = ((ProJ a,b,p) * (ProJ p,a,x)) * (ProJ x,p,y) by A1, A2, A5, A6, Def6;
hence PProJ a,b,x,(l * y) = l * (PProJ a,b,x,y) by A7, GROUP_1:def 4; :: thesis: verum

end;

now

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

end;

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