let F be Field; :: thesis: for S being SymSp of F
for p, a, x, q, b, y being Element of S st (1_ F) + (1_ F) <> 0. F & 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 SymSp of F; :: thesis: for p, a, x, q, b, y being Element of S st (1_ F) + (1_ F) <> 0. F & 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: ( (1_ F) + (1_ F) <> 0. F & 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 A1: ( (1_ F) + (1_ F) <> 0. F & not a _|_ & not x _|_ & not a _|_ & not x _|_ & 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)

A2: now

assume 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 & ProJ x,q,y = 0. F ) by A1, Th36;
then ( ((ProJ a,b,p) * (ProJ p,a,x)) * (ProJ x,p,y) = 0. F & ((ProJ a,b,q) * (ProJ q,a,x)) * (ProJ x,q,y) = 0. F ) by VECTSP_1:39;
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) ; :: thesis: verum

end;

now

assume A3: 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, Th42;
then ((ProJ a,b,p) * ((ProJ a,b,q) " )) * (ProJ p,a,x) = (ProJ x,q,p) * (ProJ q,a,x) by A1, Th37;
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 A1, A3, Th37;
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 A4: ((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;
ProJ a,b,q <> 0. F by A1, Th36;
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 A4, 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 A1, A3, Th38;
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 A5: ((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 A1, A3, Th36;
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 A5, 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 A1, A3, Th38;
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;

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 A2; :: thesis: verum