theorem Th1: :: NDIFF12:1

for E, F, G being RealNormSpace
for f being BilinearOperator of E,F,G
for z being Point of [:E,F:] holds
( f * (reproj1 z) is LinearOperator of E,G & f * (reproj2 z) is LinearOperator of F,G )