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;

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)

hence
QFunctional (f,W) is cmplxhomogeneous
; :: thesis: verumfor 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;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