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