:: deftheorem defines Bilinear LOPBAN_8:def 1 :
for E, F, G being RealLinearSpace
for f being Function of [: the carrier of E, the carrier of F:], the carrier of G holds
( f is Bilinear iff ( ( for v being Point of E st v in dom (curry f) holds
(curry f) . v is additive homogeneous Function of F,G ) & ( for v being Point of F st v in dom (curry' f) holds
(curry' f) . v is additive homogeneous Function of E,G ) ) );