let F be Field; :: thesis: for S being SymSp of F
for p, a, x, q being Element of S st (1_ F) + (1_ F) <> 0. F & not a _|_ & not x _|_ & not a _|_ & not x _|_ holds
(ProJ a,q,p) * (ProJ p,a,x) = (ProJ x,q,p) * (ProJ q,a,x)
let S be SymSp of F; :: thesis: for p, a, x, q being Element of S st (1_ F) + (1_ F) <> 0. F & not a _|_ & not x _|_ & not a _|_ & not x _|_ holds
(ProJ a,q,p) * (ProJ p,a,x) = (ProJ x,q,p) * (ProJ q,a,x)
let p, a, x, q be Element of S; :: thesis: ( (1_ F) + (1_ F) <> 0. F & not a _|_ & not x _|_ & not a _|_ & not x _|_ implies (ProJ a,q,p) * (ProJ p,a,x) = (ProJ x,q,p) * (ProJ q,a,x) )
set 0F = 0. F;
set 1F = 1_ F;
assume that
A1: (1_ F) + (1_ F) <> 0. F and
A2: not a _|_ and
A3: not x _|_ and
A4: not a _|_ and
A5: not x _|_ ; :: thesis: (ProJ a,q,p) * (ProJ p,a,x) = (ProJ x,q,p) * (ProJ q,a,x)
A6: ( not q _|_ & not q _|_ ) by A4, A5, Th12;
(ProJ p,a,x) * (ProJ q,x,a) = (ProJ a,p,q) * (ProJ x,q,p) by A1, A2, A3, A5, Th41;
then (ProJ p,a,x) * (ProJ q,x,a) = ((ProJ a,q,p) " ) * (ProJ x,q,p) by A2, A4, Th38;
then A7: (ProJ a,q,p) * ((ProJ p,a,x) * (ProJ q,x,a)) = ((ProJ a,q,p) * ((ProJ a,q,p) " )) * (ProJ x,q,p) by GROUP_1:def 4;
ProJ a,q,p <> 0. F by A2, A4, Th36;
then (ProJ a,q,p) * ((ProJ p,a,x) * (ProJ q,x,a)) = (ProJ x,q,p) * (1_ F) by A7, VECTSP_1:def 22;
then (ProJ a,q,p) * ((ProJ p,a,x) * (ProJ q,x,a)) = ProJ x,q,p by VECTSP_1:def 19;
then ((ProJ a,q,p) * (ProJ p,a,x)) * (ProJ q,x,a) = ProJ x,q,p by GROUP_1:def 4;
then ((ProJ a,q,p) * (ProJ p,a,x)) * ((ProJ q,a,x) " ) = ProJ x,q,p by A6, Th38;
then A8: ((ProJ a,q,p) * (ProJ p,a,x)) * (((ProJ q,a,x) " ) * (ProJ q,a,x)) = (ProJ x,q,p) * (ProJ q,a,x) by GROUP_1:def 4;
ProJ q,a,x <> 0. F by A6, Th36;
then ((ProJ a,q,p) * (ProJ p,a,x)) * (1_ F) = (ProJ x,q,p) * (ProJ q,a,x) by A8, VECTSP_1:def 22;
hence (ProJ a,q,p) * (ProJ p,a,x) = (ProJ x,q,p) * (ProJ q,a,x) by VECTSP_1:def 19; :: thesis: verum