let V, W be non empty VectSpStr of 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 by Def4;
thus f . v1,(r * w) = (FunctionalFAF f,v1) . (r * w) by BILINEAR:9
.= (r *' ) * ((FunctionalFAF f,v1) . w) by A1, Def1
.= (r *' ) * (f . v1,w) by BILINEAR:9 ; :: thesis: verum