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
set vq = VectQuot (V,W);
set qf = QFunctional (f,W);
A2: ker (f *') = ker f by Th23;

now :: thesis: for A being Vector of (VectQuot (V,W))
for r being Scalar of holds (QFunctional (f,W)) . (r * A) = (r *') * ((QFunctional (f,W)) . A)

set C = CosetSet (V,W);
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)
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 ; :: thesis: verum