let V, W be non empty ModuleStr over F_Complex ; :: thesis: for v being Vector of V

for w being Vector of W

for a being Element of F_Complex

for f being Form of V,W st f is cmplxhomogeneousFAF holds

f . (v,(a * w)) = (a *') * (f . (v,w))

let v1 be Vector of V; :: thesis: for w being Vector of W

for a being Element of F_Complex

for f being Form of V,W st f is cmplxhomogeneousFAF holds

f . (v1,(a * w)) = (a *') * (f . (v1,w))

let w be Vector of W; :: thesis: for a being Element of F_Complex

for f being Form of V,W st f is cmplxhomogeneousFAF holds

f . (v1,(a * w)) = (a *') * (f . (v1,w))

let r be Element of F_Complex; :: thesis: for f being Form of V,W st f is cmplxhomogeneousFAF holds

f . (v1,(r * w)) = (r *') * (f . (v1,w))

let f be Form of V,W; :: thesis: ( f is cmplxhomogeneousFAF implies f . (v1,(r * w)) = (r *') * (f . (v1,w)) )

set F = FunctionalFAF (f,v1);

assume f is cmplxhomogeneousFAF ; :: thesis: f . (v1,(r * w)) = (r *') * (f . (v1,w))

then A1: FunctionalFAF (f,v1) is cmplxhomogeneous ;

thus f . (v1,(r * w)) = (FunctionalFAF (f,v1)) . (r * w) by BILINEAR:8

.= (r *') * ((FunctionalFAF (f,v1)) . w) by A1

.= (r *') * (f . (v1,w)) by BILINEAR:8 ; :: thesis: verum

for w being Vector of W

for a being Element of F_Complex

for f being Form of V,W st f is cmplxhomogeneousFAF holds

f . (v,(a * w)) = (a *') * (f . (v,w))

let v1 be Vector of V; :: thesis: for w being Vector of W

for a being Element of F_Complex

for f being Form of V,W st f is cmplxhomogeneousFAF holds

f . (v1,(a * w)) = (a *') * (f . (v1,w))

let w be Vector of W; :: thesis: for a being Element of F_Complex

for f being Form of V,W st f is cmplxhomogeneousFAF holds

f . (v1,(a * w)) = (a *') * (f . (v1,w))

let r be Element of F_Complex; :: thesis: for f being Form of V,W st f is cmplxhomogeneousFAF holds

f . (v1,(r * w)) = (r *') * (f . (v1,w))

let f be Form of V,W; :: thesis: ( f is cmplxhomogeneousFAF implies f . (v1,(r * w)) = (r *') * (f . (v1,w)) )

set F = FunctionalFAF (f,v1);

assume f is cmplxhomogeneousFAF ; :: thesis: f . (v1,(r * w)) = (r *') * (f . (v1,w))

then A1: FunctionalFAF (f,v1) is cmplxhomogeneous ;

thus f . (v1,(r * w)) = (FunctionalFAF (f,v1)) . (r * w) by BILINEAR:8

.= (r *') * ((FunctionalFAF (f,v1)) . w) by A1

.= (r *') * (f . (v1,w)) by BILINEAR:8 ; :: thesis: verum