theorem :: SYMSP_1:35

for F being Field
for S being SymSp of F
for a, b, x, y being Element of S
for l being Element of F st (1_ F) + (1_ F) <> 0. F & not a _|_ holds
PProJ (a,b,x,(l * y)) = l * (PProJ (a,b,x,y))