theorem Th28: :: SYMSP_1:28

for F being Field
for S being SymSp of F
for a, b, p, q 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))