let V, W be non empty ModuleStr over INT.Ring ; :: thesis: for f being FrFunctional of V
for g being FrFunctional of W
for v being Vector of V holds FrFunctionalFAF ((FrFormFunctional (f,g)),v) = (f . v) * g
let f be FrFunctional of V; :: thesis: for g being FrFunctional of W
for v being Vector of V holds FrFunctionalFAF ((FrFormFunctional (f,g)),v) = (f . v) * g
let h be FrFunctional of W; :: thesis: for v being Vector of V holds FrFunctionalFAF ((FrFormFunctional (f,h)),v) = (f . v) * h
let v be Vector of V; :: thesis: FrFunctionalFAF ((FrFormFunctional (f,h)),v) = (f . v) * h
set F = FrFormFunctional (f,h);
set FF = FrFunctionalFAF ((FrFormFunctional (f,h)),v);

now :: thesis: for y being Vector of W holds (FrFunctionalFAF ((FrFormFunctional (f,h)),v)) . y = ((f . v) * h) . y

let y be Vector of W; :: thesis: (FrFunctionalFAF ((FrFormFunctional (f,h)),v)) . y = ((f . v) * h) . y
thus (FrFunctionalFAF ((FrFormFunctional (f,h)),v)) . y = (FrFormFunctional (f,h)) . (v,y) by HTh8
.= (f . v) * (h . y) by HDef10
.= ((f . v) * h) . y by HDef6 ; :: thesis: verum

end;

hence FrFunctionalFAF ((FrFormFunctional (f,h)),v) = (f . v) * h by FUNCT_2:63; :: thesis: verum