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