let K be non empty multMagma ; :: thesis: 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; :: 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 ;

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 ; :: thesis: verum

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; :: 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 ;

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 ; :: thesis: verum