let F be Field; :: thesis: for S being OrtSp of F
for a, b, p, q, x, y being Element of S st not a _|_ & not x _|_ & not a _|_ & not x _|_ & not a _|_ holds
((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y))
let S be OrtSp of F; :: thesis: for a, b, p, q, x, y being Element of S st not a _|_ & not x _|_ & not a _|_ & not x _|_ & not a _|_ holds
((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y))
let a, b, p, q, x, y be Element of S; :: thesis: ( not a _|_ & not x _|_ & not a _|_ & not x _|_ & not a _|_ implies ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) )
set 0F = 0. F;
set 1F = 1_ F;
assume that
A1: not a _|_ and
A2: not x _|_ and
A3: not a _|_ and
A4: not x _|_ and
A5: not a _|_ ; :: thesis: ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y))

A6: now :: thesis: ( not x _|_ implies ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) )

A7: ProJ (a,b,q) <> 0. F by A3, A5, Th20;
assume A8: not x _|_ ; :: thesis: ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y))
(ProJ (a,q,p)) * (ProJ (p,a,x)) = (ProJ (x,q,p)) * (ProJ (q,a,x)) by A1, A2, A3, A4, Th25;
then ((ProJ (a,b,p)) * ((ProJ (a,b,q)) ")) * (ProJ (p,a,x)) = (ProJ (x,q,p)) * (ProJ (q,a,x)) by A3, A5, Th21;
then (((ProJ (a,b,q)) ") * (ProJ (a,b,p))) * (ProJ (p,a,x)) = ((ProJ (x,y,p)) * ((ProJ (x,y,q)) ")) * (ProJ (q,a,x)) by A4, A8, Th21;
then (ProJ (a,b,q)) * (((ProJ (a,b,q)) ") * ((ProJ (a,b,p)) * (ProJ (p,a,x)))) = (ProJ (a,b,q)) * (((ProJ (x,y,p)) * ((ProJ (x,y,q)) ")) * (ProJ (q,a,x))) by GROUP_1:def 3;
then ((ProJ (a,b,q)) * ((ProJ (a,b,q)) ")) * ((ProJ (a,b,p)) * (ProJ (p,a,x))) = (ProJ (a,b,q)) * (((ProJ (x,y,p)) * ((ProJ (x,y,q)) ")) * (ProJ (q,a,x))) by GROUP_1:def 3;
then ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (1_ F) = (ProJ (a,b,q)) * (((ProJ (x,y,p)) * ((ProJ (x,y,q)) ")) * (ProJ (q,a,x))) by A7, VECTSP_1:def 10;
then (ProJ (a,b,p)) * (ProJ (p,a,x)) = (ProJ (a,b,q)) * (((ProJ (x,y,p)) * ((ProJ (x,y,q)) ")) * (ProJ (q,a,x))) ;
then (ProJ (a,b,p)) * (ProJ (p,a,x)) = (ProJ (a,b,q)) * ((((ProJ (x,y,q)) ") * ((ProJ (x,p,y)) ")) * (ProJ (q,a,x))) by A2, A8, Th22;
then (ProJ (a,b,p)) * (ProJ (p,a,x)) = ((ProJ (a,b,q)) * (((ProJ (x,y,q)) ") * ((ProJ (x,p,y)) "))) * (ProJ (q,a,x)) by GROUP_1:def 3;
then (ProJ (a,b,p)) * (ProJ (p,a,x)) = (ProJ (q,a,x)) * (((ProJ (a,b,q)) * ((ProJ (x,y,q)) ")) * ((ProJ (x,p,y)) ")) by GROUP_1:def 3;
then ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) = (((ProJ (q,a,x)) * ((ProJ (a,b,q)) * ((ProJ (x,y,q)) "))) * ((ProJ (x,p,y)) ")) * (ProJ (x,p,y)) by GROUP_1:def 3;
then A9: ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) = ((ProJ (q,a,x)) * ((ProJ (a,b,q)) * ((ProJ (x,y,q)) "))) * (((ProJ (x,p,y)) ") * (ProJ (x,p,y))) by GROUP_1:def 3;
ProJ (x,p,y) <> 0. F by A2, A8, Th20;
then ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) = ((ProJ (q,a,x)) * ((ProJ (a,b,q)) * ((ProJ (x,y,q)) "))) * (1_ F) by A9, VECTSP_1:def 10;
then ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) = (ProJ (q,a,x)) * ((ProJ (a,b,q)) * ((ProJ (x,y,q)) ")) ;
then ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) = (ProJ (q,a,x)) * ((ProJ (a,b,q)) * (ProJ (x,q,y))) by A4, A8, Th22;
hence ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) by GROUP_1:def 3; :: thesis: verum

end;

now :: thesis: ( x _|_ implies ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) )

assume A10: x _|_ ; :: thesis: ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y))
then ProJ (x,p,y) = 0. F by A2, Th20;
then A11: ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) = 0. F ;
ProJ (x,q,y) = 0. F by A4, A10, Th20;
hence ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) by A11; :: thesis: verum

end;

hence ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) by A6; :: thesis: verum