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 homogeneousSAF holds
f . (a * v),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 homogeneousSAF holds
f . (a * v),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 homogeneousSAF holds
f . (a * v),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 homogeneousSAF holds
f . (a * v),y = a * (f . v,y)
let r be Element of K; :: thesis: for f being Form of V,W st f is homogeneousSAF holds
f . (r * v),y = r * (f . v,y)
let f be Form of V,W; :: thesis: ( f is homogeneousSAF implies f . (r * v),y = r * (f . v,y) )
set F = FunctionalSAF f,y;
assume f is homogeneousSAF ; :: thesis: f . (r * v),y = r * (f . v,y)
then A1: FunctionalSAF f,y is homogeneous by Def15;
thus f . (r * v),y = (FunctionalSAF f,y) . (r * v) by Th10
.= r * ((FunctionalSAF f,y) . v) by A1, HAHNBAN1:def 12
.= r * (f . v,y) by Th10 ; :: thesis: verum