let V, W be non empty ModuleStr over INT.Ring ; 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; 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; for w being Vector of W holds FrFunctionalSAF ((FrFormFunctional (f,h)),w) = (h . w) * f
let y be Vector of W; FrFunctionalSAF ((FrFormFunctional (f,h)),y) = (h . y) * f
set F = FrFormFunctional (f,h);
set FF = FrFunctionalSAF ((FrFormFunctional (f,h)),y);
hence
FrFunctionalSAF ((FrFormFunctional (f,h)),y) = (h . y) * f
by FUNCT_2:63; verum