let V be VectSp of F_Complex ; :: thesis: for W being Subspace of V
for f being antilinear-Functional of V st the carrier of W c= ker (f *' ) holds
QFunctional f,W is cmplxhomogeneous
let W be Subspace of V; :: thesis: for f being antilinear-Functional of V st the carrier of W c= ker (f *' ) holds
QFunctional f,W is cmplxhomogeneous
let f be antilinear-Functional of V; :: thesis: ( the carrier of W c= ker (f *' ) implies QFunctional f,W is cmplxhomogeneous )
assume A1: the carrier of W c= ker (f *' ) ; :: thesis: QFunctional f,W is cmplxhomogeneous
A2: ker (f *' ) = ker f by Th26;
set qf = QFunctional f,W;
set vq = VectQuot V,W;

now

let A be Vector of (VectQuot V,W); :: thesis: for r being Scalar of holds (QFunctional f,W) . (r * A) = (r *' ) * ((QFunctional f,W) . A)
let r be Scalar of ; :: thesis: (QFunctional f,W) . (r * A) = (r *' ) * ((QFunctional f,W) . A)
set C = CosetSet V,W;
A3: CosetSet V,W = the carrier of (VectQuot V,W) by VECTSP10:def 6;
then A in CosetSet V,W ;
then consider aa being Coset of W such that
A4: A = aa ;
consider a being Vector of V such that
A5: aa = a + W by VECTSP_4:def 6;
r * A = (lmultCoset V,W) . r,A by VECTSP10:def 6
.= (r * a) + W by A3, A4, A5, VECTSP10:def 5 ;
hence (QFunctional f,W) . (r * A) = f . (r * a) by A1, A2, VECTSP10:def 12
.= (r *' ) * (f . a) by Def1
.= (r *' ) * ((QFunctional f,W) . A) by A1, A2, A4, A5, VECTSP10:def 12 ;
:: thesis: verum

end;

hence QFunctional f,W is cmplxhomogeneous by Def1; :: thesis: verum