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

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

let v be Vector of V; :: thesis: (FunctionalSAF ((FormFunctional (f,h)),y)) . v = ((h . y) * f) . v
thus (FunctionalSAF ((FormFunctional (f,h)),y)) . v = (FormFunctional (f,h)) . (v,y) by BLTh9
.= (f . v) * (h . y) by BLDef10
.= ((h . y) * f) . v by HAHNBAN1:def 6 ; :: thesis: verum

end;

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