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

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

let v be Vector of V; :: thesis: (FrFunctionalSAF ((FrFormFunctional (f,h)),y)) . v = ((h . y) * f) . v
thus (FrFunctionalSAF ((FrFormFunctional (f,h)),y)) . v = (FrFormFunctional (f,h)) . (v,y) by HTh9
.= (f . v) * (h . y) by HDef10
.= ((h . y) * f) . v by HDef6 ; :: thesis: verum

end;

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