theorem Th26: :: SYMSP_1:26

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