let K be non empty multMagma ; :: thesis: for V, W being non empty VectSpStr of K
for f being Functional of V
for g being Functional of W
for v being Vector of V holds FunctionalFAF (FormFunctional f,g),v = (f . v) * g
let V, W be non empty VectSpStr of K; :: thesis: for f being Functional of V
for g being Functional of W
for v being Vector of V holds FunctionalFAF (FormFunctional f,g),v = (f . v) * g
let f be Functional of V; :: thesis: for g being Functional of W
for v being Vector of V holds FunctionalFAF (FormFunctional f,g),v = (f . v) * g
let h be Functional of W; :: thesis: for v being Vector of V holds FunctionalFAF (FormFunctional f,h),v = (f . v) * h
let v be Vector of V; :: thesis: FunctionalFAF (FormFunctional f,h),v = (f . v) * h
set F = FormFunctional f,h;
set FF = FunctionalFAF (FormFunctional f,h),v;

now

let y be Vector of W; :: thesis: (FunctionalFAF (FormFunctional f,h),v) . y = ((f . v) * h) . y
thus (FunctionalFAF (FormFunctional f,h),v) . y = (FormFunctional f,h) . v,y by Th9
.= (f . v) * (h . y) by Def11
.= ((f . v) * h) . y by HAHNBAN1:def 9 ; :: thesis: verum

end;

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