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

A5: now

assume that
A6: q _|_ and
A7: b _|_ ; :: thesis: (ProJ a,p,q) * (ProJ b,q,p) = (ProJ p,a,b) * (ProJ q,b,a)
not b _|_ by A4, Th12;
then A8: ProJ b,q,p = ProJ b,q,(p + a) by A7, Th32;
A9: not q _|_ by A3, A6, Th14;
then A10: ProJ b,q,(p + a) = (- ((ProJ q,(p + a),b) " )) * (ProJ (p + a),q,b) by A4, Th40;
A11: a _|_ by A1, Th25;
A12: not a _|_ by A2, Th12;
then A13: ProJ a,p,q = ProJ a,(p + a),q by A11, Th32;
not a _|_ by A12, A11, Th14;
then A14: not p + a _|_ by Th12;
A15: not p + a _|_ by A9, Th12;
then ProJ a,(p + a),q = (- ((ProJ (p + a),q,a) " )) * (ProJ q,(p + a),a) by A14, Th40;
then (ProJ a,p,q) * (ProJ b,q,p) = (((ProJ q,(p + a),a) * (- ((ProJ (p + a),q,a) " ))) * (- ((ProJ q,(p + a),b) " ))) * (ProJ (p + a),q,b) by A13, A8, A10, GROUP_1:def 4
.= ((ProJ q,(p + a),a) * ((- ((ProJ (p + a),q,a) " )) * (- ((ProJ q,(p + a),b) " )))) * (ProJ (p + a),q,b) by GROUP_1:def 4
.= ((ProJ q,(p + a),a) * (((ProJ q,(p + a),b) " ) * ((ProJ (p + a),q,a) " ))) * (ProJ (p + a),q,b) by VECTSP_1:42
.= (((ProJ q,(p + a),a) * ((ProJ q,(p + a),b) " )) * ((ProJ (p + a),q,a) " )) * (ProJ (p + a),q,b) by GROUP_1:def 4
.= ((ProJ q,b,a) * ((ProJ (p + a),q,a) " )) * (ProJ (p + a),q,b) by A4, A9, Th37
.= (ProJ q,b,a) * ((ProJ (p + a),q,b) * ((ProJ (p + a),q,a) " )) by GROUP_1:def 4
.= (ProJ q,b,a) * (ProJ (p + a),a,b) by A14, A15, Th37
.= (ProJ q,b,a) * (ProJ p,a,b) by A2, A7, A11, Th33 ;
hence (ProJ a,p,q) * (ProJ b,q,p) = (ProJ p,a,b) * (ProJ q,b,a) ; :: thesis: verum

end;

A16: now

assume A17: not b _|_ ; :: thesis: (ProJ a,p,q) * (ProJ b,q,p) = (ProJ p,a,b) * (ProJ q,b,a)
A18: not b _|_ by A4, Th12;
then A19: ProJ q,b,a = (- ((ProJ b,a,q) " )) * (ProJ a,b,q) by A17, Th40;
A20: not a _|_ by A2, Th12;
A21: not a _|_ by A17, Th12;
then ProJ p,a,b = (- ((ProJ a,b,p) " )) * (ProJ b,a,p) by A20, Th40;
then (ProJ p,a,b) * (ProJ q,b,a) = (((ProJ b,a,p) * (- ((ProJ a,b,p) " ))) * (- ((ProJ b,a,q) " ))) * (ProJ a,b,q) by A19, GROUP_1:def 4
.= ((ProJ b,a,p) * ((- ((ProJ a,b,p) " )) * (- ((ProJ b,a,q) " )))) * (ProJ a,b,q) by GROUP_1:def 4
.= ((ProJ b,a,p) * (((ProJ b,a,q) " ) * ((ProJ a,b,p) " ))) * (ProJ a,b,q) by VECTSP_1:42
.= (((ProJ b,a,p) * ((ProJ b,a,q) " )) * ((ProJ a,b,p) " )) * (ProJ a,b,q) by GROUP_1:def 4
.= ((ProJ b,q,p) * ((ProJ a,b,p) " )) * (ProJ a,b,q) by A17, A18, Th37
.= (ProJ b,q,p) * ((ProJ a,b,q) * ((ProJ a,b,p) " )) by GROUP_1:def 4
.= (ProJ b,q,p) * (ProJ a,p,q) by A21, A20, Th37 ;
hence (ProJ a,p,q) * (ProJ b,q,p) = (ProJ p,a,b) * (ProJ q,b,a) ; :: thesis: verum

end;

now

assume A22: not q _|_ ; :: thesis: (ProJ a,p,q) * (ProJ b,q,p) = (ProJ p,a,b) * (ProJ q,b,a)
then A23: ProJ b,q,p = (- ((ProJ q,p,b) " )) * (ProJ p,q,b) by A4, Th40;
A24: not p _|_ by A22, Th12;
then ProJ a,p,q = (- ((ProJ p,q,a) " )) * (ProJ q,p,a) by A2, Th40;
then (ProJ a,p,q) * (ProJ b,q,p) = (((ProJ q,p,a) * (- ((ProJ p,q,a) " ))) * (- ((ProJ q,p,b) " ))) * (ProJ p,q,b) by A23, GROUP_1:def 4
.= ((ProJ q,p,a) * ((- ((ProJ p,q,a) " )) * (- ((ProJ q,p,b) " )))) * (ProJ p,q,b) by GROUP_1:def 4
.= ((ProJ q,p,a) * (((ProJ q,p,b) " ) * ((ProJ p,q,a) " ))) * (ProJ p,q,b) by VECTSP_1:42
.= (((ProJ q,p,a) * ((ProJ q,p,b) " )) * ((ProJ p,q,a) " )) * (ProJ p,q,b) by GROUP_1:def 4
.= ((ProJ q,b,a) * ((ProJ p,q,a) " )) * (ProJ p,q,b) by A4, A22, Th37
.= (ProJ q,b,a) * ((ProJ p,q,b) * ((ProJ p,q,a) " )) by GROUP_1:def 4
.= (ProJ q,b,a) * (ProJ p,a,b) by A2, A24, Th37 ;
hence (ProJ a,p,q) * (ProJ b,q,p) = (ProJ p,a,b) * (ProJ q,b,a) ; :: thesis: verum

end;

hence (ProJ a,p,q) * (ProJ b,q,p) = (ProJ p,a,b) * (ProJ q,b,a) by A16, A5; :: thesis: verum