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

A7: ProJ (a,b,q) <> 0. F by A3, A5, Th33;
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, Th38;
then ((ProJ (a,b,p)) * ((ProJ (a,b,q)) ")) * (ProJ (p,a,x)) = (ProJ (x,q,p)) * (ProJ (q,a,x)) by A3, A5, Th34;
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, Th34;
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))) by VECTSP_1:def 8;
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, Th35;
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, Th33;
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)) ")) by VECTSP_1:def 8;
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, Th35;
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

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, Th33;
then A11: ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) = 0. F by VECTSP_1:7;
ProJ (x,q,y) = 0. F by A4, A10, Th33;
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, VECTSP_1:7; :: 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