let F be Field; :: thesis: for S being OrtSp of F
for b, a, 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 b, a, x, y being Element of S st not a _|_ holds
PProJ a,b,x,y = PProJ a,b,y,x
let b, a, 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

assume not y _|_ ; :: thesis: PProJ a,b,x,y = PProJ a,b,y,x
then A3: ( x <> 0. S & y <> 0. S ) by Th11, Th12;
a <> 0. S by A1, Th11, Th12;
then ex r being Element of S st
( not a _|_ & not x _|_ & not y _|_ & not a _|_ ) by A3, Def2;
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, Th12;
PProJ a,b,y,x = ((ProJ a,b,r) * (ProJ r,a,y)) * (ProJ y,r,x) by A1, A4, A6, Def7;
then A8: PProJ a,b,y,x = (ProJ a,b,r) * ((ProJ r,a,y) * (ProJ y,r,x)) by GROUP_1:def 4;
( not r _|_ & not r _|_ ) by A4, A5, Th12;
then A9: PProJ a,b,y,x = (ProJ a,b,r) * ((ProJ r,a,x) * (ProJ x,r,y)) by A7, A8, Th40;
PProJ a,b,x,y = ((ProJ a,b,r) * (ProJ r,a,x)) * (ProJ x,r,y) by A1, A4, A5, Def7;
hence PProJ a,b,x,y = PProJ a,b,y,x by A9, GROUP_1:def 4; :: thesis: verum

end;

now

assume y _|_ ; :: thesis: PProJ a,b,x,y = PProJ a,b,y,x
then ( x _|_ & PProJ a,b,y,x = 0. F ) by A1, Th12, Th44;
hence PProJ a,b,x,y = PProJ a,b,y,x by A1, Th44; :: thesis: verum

end;

hence PProJ a,b,x,y = PProJ a,b,y,x by A2; :: thesis: verum