let K be non empty multMagma ; :: thesis: for V, W being non empty VectSpStr of 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 VectSpStr of 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 by Def14;
thus f . v,(r * y) = (FunctionalFAF f,v) . (r * y) by Th9
.= r * ((FunctionalFAF f,v) . y) by A1, HAHNBAN1:def 12
.= r * (f . v,y) by Th9 ; :: thesis: verum