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

for a, b, x, y being Element of S st not a _|_ holds

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

let S be OrtSp of F; :: thesis: for a, b, x, y being Element of S st not a _|_ holds

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

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

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

for a, b, x, y being Element of S st not a _|_ holds

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

let S be OrtSp of F; :: thesis: for a, b, x, y being Element of S st not a _|_ holds

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

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

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

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

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

then A3: ( x <> 0. S & y <> 0. S ) by Th1, Th2;

a <> 0. S by A1, Th1, Th2;

then ex r being Element of S st

( not a _|_ & not x _|_ & not y _|_ & not a _|_ ) by A3, Def1;

then consider r being Element of S such that

A4: not a _|_ and

A5: not x _|_ and

A6: not y _|_ ;

A7: not r _|_ by A6, Th2;

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

then A8: PProJ (a,b,y,x) = (ProJ (a,b,r)) * ((ProJ (r,a,y)) * (ProJ (y,r,x))) by GROUP_1:def 3;

( not r _|_ & not r _|_ ) by A4, A5, Th2;

then A9: PProJ (a,b,y,x) = (ProJ (a,b,r)) * ((ProJ (r,a,x)) * (ProJ (x,r,y))) by A7, A8, Th27;

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

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

end;then A3: ( x <> 0. S & y <> 0. S ) by Th1, Th2;

a <> 0. S by A1, Th1, Th2;

then ex r being Element of S st

( not a _|_ & not x _|_ & not y _|_ & not a _|_ ) by A3, Def1;

then consider r being Element of S such that

A4: not a _|_ and

A5: not x _|_ and

A6: not y _|_ ;

A7: not r _|_ by A6, Th2;

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

then A8: PProJ (a,b,y,x) = (ProJ (a,b,r)) * ((ProJ (r,a,y)) * (ProJ (y,r,x))) by GROUP_1:def 3;

( not r _|_ & not r _|_ ) by A4, A5, Th2;

then A9: PProJ (a,b,y,x) = (ProJ (a,b,r)) * ((ProJ (r,a,x)) * (ProJ (x,r,y))) by A7, A8, Th27;

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

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

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

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

then ( x _|_ & PProJ (a,b,y,x) = 0. F ) by A1, Th2, Th29;

hence PProJ (a,b,x,y) = PProJ (a,b,y,x) by A1, Th29; :: thesis: verum

end;then ( x _|_ & PProJ (a,b,y,x) = 0. F ) by A1, Th2, Th29;

hence PProJ (a,b,x,y) = PProJ (a,b,y,x) by A1, Th29; :: thesis: verum