let K be non empty commutative multMagma ; :: thesis: for V, W being non empty VectSpStr of 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 VectSpStr of K; :: 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

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 Th10
.= (f . v) * (h . y) by Def11
.= ((h . y) * f) . v by HAHNBAN1:def 9 ; :: thesis: verum

end;

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