let K be non empty multMagma ; 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 homogeneousSAF holds
f . ((a * v),w) = a * (f . (v,w))
let V, W be 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 homogeneousSAF holds
f . ((a * v),w) = a * (f . (v,w))
let v be 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 y be Vector of W; 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; 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; ( f is homogeneousSAF implies f . ((r * v),y) = r * (f . (v,y)) )
set F = FunctionalSAF (f,y);
assume
f is homogeneousSAF
; f . ((r * v),y) = r * (f . (v,y))
then A1:
FunctionalSAF (f,y) is homogeneous
;
thus f . ((r * v),y) =
(FunctionalSAF (f,y)) . (r * v)
by Th9
.=
r * ((FunctionalSAF (f,y)) . v)
by A1
.=
r * (f . (v,y))
by Th9
; verum