let V, W be non empty ModuleStr over INT.Ring ; :: thesis: for v being Vector of V
for w being Vector of W
for a being Element of INT.Ring
for f being FrForm 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 INT.Ring
for f being FrForm 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 INT.Ring
for f being FrForm of V,W st f is homogeneousSAF holds
f . ((a * v),y) = a * (f . (v,y))
let r be Element of INT.Ring; :: thesis: for f being FrForm of V,W st f is homogeneousSAF holds
f . ((r * v),y) = r * (f . (v,y))
let f be FrForm of V,W; :: thesis: ( f is homogeneousSAF implies f . ((r * v),y) = r * (f . (v,y)) )
set F = FrFunctionalSAF (f,y);
assume f is homogeneousSAF ; :: thesis: f . ((r * v),y) = r * (f . (v,y))
then A1: FrFunctionalSAF (f,y) is homogeneous ;
thus f . ((r * v),y) = (FrFunctionalSAF (f,y)) . (r * v) by HTh9
.= r * ((FrFunctionalSAF (f,y)) . v) by A1
.= r * (f . (v,y)) by HTh9 ; :: thesis: verum