:: deftheorem defines Bilinear LOPBAN_8:def 2 :
for E, F, G being RealLinearSpace
for f being Function of [:E,F:],G holds
( f is Bilinear iff ex g being Function of [: the carrier of E, the carrier of F:], the carrier of G st
( f = g & g is Bilinear ) );