let F be Field; :: thesis: for S being OrtSp of F
for a, p, q, x being Element of S st not a _|_ & not x _|_ & not a _|_ & not x _|_ holds
(ProJ (a,q,p)) * (ProJ (p,a,x)) = (ProJ (q,a,x)) * (ProJ (x,q,p))

let S be OrtSp of F; :: thesis: for a, p, q, x being Element of S st not a _|_ & not x _|_ & not a _|_ & not x _|_ holds
(ProJ (a,q,p)) * (ProJ (p,a,x)) = (ProJ (q,a,x)) * (ProJ (x,q,p))

let a, p, q, x be Element of S; :: thesis: ( not a _|_ & not x _|_ & not a _|_ & not x _|_ implies (ProJ (a,q,p)) * (ProJ (p,a,x)) = (ProJ (q,a,x)) * (ProJ (x,q,p)) )
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 _|_ ; :: thesis: (ProJ (a,q,p)) * (ProJ (p,a,x)) = (ProJ (q,a,x)) * (ProJ (x,q,p))
A5: ( p <> 0. S & q <> 0. S ) by A1, A3, Th1;
A6: not p _|_ by ;
( a <> 0. S & x <> 0. S ) by A1, A2, Th1, Th2;
then consider r being Element of S such that
A7: not p _|_ and
A8: not q _|_ and
A9: not a _|_ and
A10: not x _|_ by ;
A11: not r _|_ by ;
A12: not r _|_ by ;
A13: not r _|_ by ;
then A14: ProJ (r,q,p) <> 0. F by ;
A15: not r _|_ by ;
A16: not q _|_ by ;
A17: not p _|_ by ;
A18: not q _|_ by ;
((ProJ (a,q,p)) * (ProJ (p,a,x))) * ((ProJ (q,a,x)) ") = (((ProJ (a,r,p)) * ((ProJ (a,r,q)) ")) * (ProJ (p,a,x))) * ((ProJ (q,a,x)) ") by A3, A9, Th21
.= (((ProJ (a,r,p)) * ((ProJ (a,r,q)) ")) * ((ProJ (p,r,x)) * ((ProJ (p,r,a)) "))) * ((ProJ (q,a,x)) ") by A6, A7, Th21
.= (((ProJ (a,r,p)) * ((ProJ (a,r,q)) ")) * ((ProJ (p,r,x)) * ((ProJ (p,r,a)) "))) * (ProJ (q,x,a)) by
.= (((ProJ (a,r,p)) * ((ProJ (a,r,q)) ")) * ((ProJ (p,r,x)) * ((ProJ (p,r,a)) "))) * ((ProJ (q,r,a)) * ((ProJ (q,r,x)) ")) by
.= ((((ProJ (a,p,r)) ") * ((ProJ (a,r,q)) ")) * ((ProJ (p,r,x)) * ((ProJ (p,r,a)) "))) * ((ProJ (q,r,a)) * ((ProJ (q,r,x)) ")) by A1, A9, Th22
.= ((((ProJ (a,p,r)) ") * ((ProJ (a,r,q)) ")) * ((ProJ (p,r,x)) * (ProJ (p,a,r)))) * ((ProJ (q,r,a)) * ((ProJ (q,r,x)) ")) by A6, A7, Th22
.= ((((ProJ (a,p,r)) ") * (ProJ (a,q,r))) * ((ProJ (p,r,x)) * (ProJ (p,a,r)))) * ((ProJ (q,r,a)) * ((ProJ (q,r,x)) ")) by A3, A9, Th22
.= ((((ProJ (a,p,r)) ") * (ProJ (a,q,r))) * ((ProJ (p,r,x)) * (ProJ (p,a,r)))) * (((ProJ (q,a,r)) ") * ((ProJ (q,r,x)) ")) by
.= ((((ProJ (a,p,r)) ") * (ProJ (a,q,r))) * (((ProJ (p,x,r)) ") * (ProJ (p,a,r)))) * (((ProJ (q,a,r)) ") * ((ProJ (q,r,x)) ")) by
.= ((((ProJ (p,x,r)) ") * (ProJ (p,a,r))) * (((ProJ (a,p,r)) ") * (ProJ (a,q,r)))) * (((ProJ (q,a,r)) ") * (ProJ (q,x,r))) by
.= (((ProJ (p,x,r)) ") * ((((ProJ (a,p,r)) ") * (ProJ (a,q,r))) * (ProJ (p,a,r)))) * (((ProJ (q,a,r)) ") * (ProJ (q,x,r))) by GROUP_1:def 3
.= (((ProJ (p,x,r)) ") * ((((ProJ (a,p,r)) ") * (ProJ (p,a,r))) * (ProJ (a,q,r)))) * (((ProJ (q,a,r)) ") * (ProJ (q,x,r))) by GROUP_1:def 3
.= (((ProJ (p,x,r)) ") * ((ProJ (r,a,p)) * (ProJ (a,q,r)))) * (((ProJ (q,a,r)) ") * (ProJ (q,x,r))) by A1, A9, Th24
.= ((((ProJ (p,x,r)) ") * (ProJ (r,a,p))) * (ProJ (a,q,r))) * (((ProJ (q,a,r)) ") * (ProJ (q,x,r))) by GROUP_1:def 3
.= (((ProJ (p,x,r)) ") * (ProJ (r,a,p))) * ((ProJ (a,q,r)) * (((ProJ (q,a,r)) ") * (ProJ (q,x,r)))) by GROUP_1:def 3
.= (((ProJ (p,x,r)) ") * (ProJ (r,a,p))) * ((((ProJ (q,a,r)) ") * (ProJ (a,q,r))) * (ProJ (q,x,r))) by GROUP_1:def 3
.= (((ProJ (p,x,r)) ") * (ProJ (r,a,p))) * ((ProJ (r,q,a)) * (ProJ (q,x,r))) by
.= ((ProJ (p,x,r)) ") * ((ProJ (r,a,p)) * ((ProJ (r,q,a)) * (ProJ (q,x,r)))) by GROUP_1:def 3
.= ((ProJ (p,x,r)) ") * (((ProJ (r,a,p)) * (ProJ (r,q,a))) * (ProJ (q,x,r))) by GROUP_1:def 3
.= ((ProJ (p,x,r)) ") * (((ProJ (r,a,p)) * ((ProJ (r,a,q)) ")) * (ProJ (q,x,r))) by
.= ((ProJ (p,x,r)) ") * ((ProJ (r,q,p)) * (ProJ (q,x,r))) by
.= (ProJ (p,r,x)) * ((ProJ (r,q,p)) * (ProJ (q,x,r))) by
.= (((ProJ (r,x,p)) ") * (ProJ (x,r,p))) * ((ProJ (r,q,p)) * (ProJ (q,x,r))) by
.= (((ProJ (r,x,p)) ") * (ProJ (x,r,p))) * ((ProJ (r,q,p)) * (((ProJ (x,r,q)) ") * (ProJ (r,x,q)))) by
.= (((ProJ (r,x,p)) ") * (ProJ (x,r,p))) * ((ProJ (r,x,q)) * ((ProJ (r,q,p)) * ((ProJ (x,r,q)) "))) by GROUP_1:def 3
.= (((ProJ (x,r,p)) * ((ProJ (r,x,p)) ")) * (ProJ (r,x,q))) * ((ProJ (r,q,p)) * ((ProJ (x,r,q)) ")) by GROUP_1:def 3
.= ((ProJ (x,r,p)) * ((ProJ (r,x,q)) * ((ProJ (r,x,p)) "))) * ((ProJ (r,q,p)) * ((ProJ (x,r,q)) ")) by GROUP_1:def 3
.= ((ProJ (x,r,p)) * (ProJ (r,p,q))) * ((ProJ (r,q,p)) * ((ProJ (x,r,q)) ")) by
.= (ProJ (x,r,p)) * ((ProJ (r,p,q)) * ((ProJ (r,q,p)) * ((ProJ (x,r,q)) "))) by GROUP_1:def 3
.= (ProJ (x,r,p)) * (((ProJ (r,p,q)) * (ProJ (r,q,p))) * ((ProJ (x,r,q)) ")) by GROUP_1:def 3
.= (ProJ (x,r,p)) * ((((ProJ (r,q,p)) ") * (ProJ (r,q,p))) * ((ProJ (x,r,q)) ")) by
.= (ProJ (x,r,p)) * (((ProJ (x,r,q)) ") * (1_ F)) by
.= (ProJ (x,r,p)) * ((ProJ (x,r,q)) ")
.= ProJ (x,q,p) by ;
then A19: ((ProJ (q,a,x)) * ((ProJ (q,a,x)) ")) * ((ProJ (a,q,p)) * (ProJ (p,a,x))) = (ProJ (q,a,x)) * (ProJ (x,q,p)) by GROUP_1:def 3;
ProJ (q,a,x) <> 0. F by ;
then ((ProJ (a,q,p)) * (ProJ (p,a,x))) * (1_ F) = (ProJ (q,a,x)) * (ProJ (x,q,p)) by ;
hence (ProJ (a,q,p)) * (ProJ (p,a,x)) = (ProJ (q,a,x)) * (ProJ (x,q,p)) ; :: thesis: verum