theorem Th22: :: SYMSP_1:22

for F being Field
for S being SymSp of F
for a, b being Element of S st not a _|_ holds
ProJ (a,b,b) = 1_ F