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 4;
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 4;
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 22;
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 19;
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 4;
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 4;
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 4;
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 4;
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 22;
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 19;
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 4; :: 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:39;
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:39; :: 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