let V, W be non empty ModuleStr over INT.Ring ; :: thesis: for f being FrForm of V,W
for v being Vector of V holds
( dom (FrFunctionalFAF (f,v)) = the carrier of W & rng (FrFunctionalFAF (f,v)) c= the carrier of F_Real & ( for w being Vector of W holds (FrFunctionalFAF (f,v)) . w = f . (v,w) ) )
let f be FrForm of V,W; :: thesis: for v being Vector of V holds
( dom (FrFunctionalFAF (f,v)) = the carrier of W & rng (FrFunctionalFAF (f,v)) c= the carrier of F_Real & ( for w being Vector of W holds (FrFunctionalFAF (f,v)) . w = f . (v,w) ) )
let v be Vector of V; :: thesis: ( dom (FrFunctionalFAF (f,v)) = the carrier of W & rng (FrFunctionalFAF (f,v)) c= the carrier of F_Real & ( for w being Vector of W holds (FrFunctionalFAF (f,v)) . w = f . (v,w) ) )
set F = FrFunctionalFAF (f,v);
dom f = [: the carrier of V, the carrier of W:] by FUNCT_2:def 1;
then A1: ex g being Function st
( (curry f) . v = g & dom g = the carrier of W & rng g c= rng f & ( for y being object st y in the carrier of W holds
g . y = f . (v,y) ) ) by FUNCT_5:29;
hence ( dom (FrFunctionalFAF (f,v)) = the carrier of W & rng (FrFunctionalFAF (f,v)) c= the carrier of F_Real ) ; :: thesis: for w being Vector of W holds (FrFunctionalFAF (f,v)) . w = f . (v,w)
let y be Vector of W; :: thesis: (FrFunctionalFAF (f,v)) . y = f . (v,y)
thus (FrFunctionalFAF (f,v)) . y = f . (v,y) by A1; :: thesis: verum