let F be Field; :: thesis: for S being OrtSp of F

for a, b, x, y being Element of S

for l being Element of F st not a _|_ holds

PProJ (a,b,x,(l * y)) = l * (PProJ (a,b,x,y))

let S be OrtSp of F; :: thesis: for a, b, x, y being Element of S

for l being Element of F st 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 not a _|_ holds

PProJ (a,b,x,(l * y)) = l * (PProJ (a,b,x,y))

let l be Element of F; :: thesis: ( not a _|_ implies PProJ (a,b,x,(l * y)) = l * (PProJ (a,b,x,y)) )

set 0F = 0. F;

assume A1: not a _|_ ; :: thesis: PProJ (a,b,x,(l * y)) = l * (PProJ (a,b,x,y))

for a, b, x, y being Element of S

for l being Element of F st not a _|_ holds

PProJ (a,b,x,(l * y)) = l * (PProJ (a,b,x,y))

let S be OrtSp of F; :: thesis: for a, b, x, y being Element of S

for l being Element of F st 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 not a _|_ holds

PProJ (a,b,x,(l * y)) = l * (PProJ (a,b,x,y))

let l be Element of F; :: thesis: ( not a _|_ implies PProJ (a,b,x,(l * y)) = l * (PProJ (a,b,x,y)) )

set 0F = 0. F;

assume A1: not a _|_ ; :: thesis: PProJ (a,b,x,(l * y)) = l * (PProJ (a,b,x,y))

A2: 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 A3: x <> 0. S by Th1;

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 _|_ and

A5: not x _|_ ;

PProJ (a,b,x,(l * y)) = ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,(l * y))) by A1, A4, A5, Def3;

then A6: PProJ (a,b,x,(l * y)) = (l * (ProJ (x,p,y))) * ((ProJ (a,b,p)) * (ProJ (p,a,x))) by A5, Th12;

PProJ (a,b,x,y) = ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) by A1, A4, A5, Def3;

hence PProJ (a,b,x,(l * y)) = l * (PProJ (a,b,x,y)) by A6, GROUP_1:def 3; :: thesis: verum

end;then A3: x <> 0. S by Th1;

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 _|_ and

A5: not x _|_ ;

PProJ (a,b,x,(l * y)) = ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,(l * y))) by A1, A4, A5, Def3;

then A6: PProJ (a,b,x,(l * y)) = (l * (ProJ (x,p,y))) * ((ProJ (a,b,p)) * (ProJ (p,a,x))) by A5, Th12;

PProJ (a,b,x,y) = ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) by A1, A4, A5, Def3;

hence PProJ (a,b,x,(l * y)) = l * (PProJ (a,b,x,y)) by A6, GROUP_1:def 3; :: thesis: verum

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

hence
PProJ (a,b,x,(l * y)) = l * (PProJ (a,b,x,y))
by A2; :: thesis: verumassume A7:
y _|_
; :: thesis: PProJ (a,b,x,(l * y)) = l * (PProJ (a,b,x,y))

then x _|_ by Th2;

then x _|_ by Def1;

then A8: PProJ (a,b,x,(l * y)) = 0. F by A1, Th29;

x _|_ by A7, Th2;

then l * (PProJ (a,b,x,y)) = l * (0. F) by A1, Th29;

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

end;then x _|_ by Th2;

then x _|_ by Def1;

then A8: PProJ (a,b,x,(l * y)) = 0. F by A1, Th29;

x _|_ by A7, Th2;

then l * (PProJ (a,b,x,y)) = l * (0. F) by A1, Th29;

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