for E, F, G being RealNormSpace
for L being Function of [:E,F:],G holds
( L is Bilinear iff ( ( for x1, x2 being Point of E
for y being Point of F holds L . ((x1 + x2),y) = (L . (x1,y)) + (L . (x2,y)) ) & ( for x being Point of E
for y being Point of F
for a being Real holds L . ((a * x),y) = a * (L . (x,y)) ) & ( for x being Point of E
for y1, y2 being Point of F holds L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2)) ) & ( for x being Point of E
for y being Point of F
for a being Real holds L . (x,(a * y)) = a * (L . (x,y)) ) ) ) by LM6;