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