let K be non empty multMagma ; :: thesis: for V, W being non empty ModuleStr over K
for v being Vector of V
for w being Vector of W
for a being Element of K
for f being Form of V,W st f is homogeneousFAF holds
f . (v,(a * w)) = a * (f . (v,w))
let V, W be non empty ModuleStr over K; :: thesis: for v being Vector of V
for w being Vector of W
for a being Element of K
for f being Form of V,W st f is homogeneousFAF holds
f . (v,(a * w)) = a * (f . (v,w))
let v be Vector of V; :: thesis: for w being Vector of W
for a being Element of K
for f being Form of V,W st f is homogeneousFAF holds
f . (v,(a * w)) = a * (f . (v,w))
let y be Vector of W; :: thesis: for a being Element of K
for f being Form of V,W st f is homogeneousFAF holds
f . (v,(a * y)) = a * (f . (v,y))
let r be Element of K; :: thesis: for f being Form of V,W st f is homogeneousFAF holds
f . (v,(r * y)) = r * (f . (v,y))
let f be Form of V,W; :: thesis: ( f is homogeneousFAF implies f . (v,(r * y)) = r * (f . (v,y)) )
set F = FunctionalFAF (f,v);
assume f is homogeneousFAF ; :: thesis: f . (v,(r * y)) = r * (f . (v,y))
then A1: FunctionalFAF (f,v) is homogeneous ;
thus f . (v,(r * y)) = (FunctionalFAF (f,v)) . (r * y) by Th8
.= r * ((FunctionalFAF (f,v)) . y) by A1
.= r * (f . (v,y)) by Th8 ; :: thesis: verum