theorem Th15: :: ORTSP_1:15

for F being Field
for S being OrtSp of F
for a, b, x being Element of S
for l being Element of F st not a _|_ & l <> 0. F holds
ProJ ((l * a),b,x) = ProJ (a,b,x)