theorem Th20: :: SYMSP_1:20

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