let K be non empty commutative multMagma ; :: thesis: 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; :: 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);

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; :: 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

hence
FunctionalSAF ((FormFunctional (f,h)),y) = (h . y) * f
by FUNCT_2:63; :: thesis: verumlet 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 Th9

.= (f . v) * (h . y) by Def10

.= ((h . y) * f) . v by HAHNBAN1:def 6 ; :: thesis: verum

end;thus (FunctionalSAF ((FormFunctional (f,h)),y)) . v = (FormFunctional (f,h)) . (v,y) by Th9

.= (f . v) * (h . y) by Def10

.= ((h . y) * f) . v by HAHNBAN1:def 6 ; :: thesis: verum