let K be non empty multMagma ; :: thesis: for V, W being non empty ModuleStr over 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 ModuleStr over 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);

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 ModuleStr over 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 :: thesis: for y being Vector of W holds (FunctionalFAF ((FormFunctional (f,h)),v)) . y = ((f . v) * h) . y

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

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

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

end;thus (FunctionalFAF ((FormFunctional (f,h)),v)) . y = (FormFunctional (f,h)) . (v,y) by Th8

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

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