theorem LM8:
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;