theorem Th15: :: SYMSP_1:15

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