let V be VectSp of F_Complex ; :: thesis: for f being antilinear-Functional of V

for A being Vector of (VectQuot (V,(Ker (f *'))))

for v being Vector of V st A = v + (Ker (f *')) holds

(QcFunctional f) . A = f . v

let f be antilinear-Functional of V; :: thesis: for A being Vector of (VectQuot (V,(Ker (f *'))))

for v being Vector of V st A = v + (Ker (f *')) holds

(QcFunctional f) . A = f . v

let A be Vector of (VectQuot (V,(Ker (f *')))); :: thesis: for v being Vector of V st A = v + (Ker (f *')) holds

(QcFunctional f) . A = f . v

let v be Vector of V; :: thesis: ( A = v + (Ker (f *')) implies (QcFunctional f) . A = f . v )

assume A1: A = v + (Ker (f *')) ; :: thesis: (QcFunctional f) . A = f . v

the carrier of (Ker (f *')) = ker (f *') by VECTSP10:def 11

.= ker f by Th23 ;

hence (QcFunctional f) . A = f . v by A1, VECTSP10:def 12; :: thesis: verum

for A being Vector of (VectQuot (V,(Ker (f *'))))

for v being Vector of V st A = v + (Ker (f *')) holds

(QcFunctional f) . A = f . v

let f be antilinear-Functional of V; :: thesis: for A being Vector of (VectQuot (V,(Ker (f *'))))

for v being Vector of V st A = v + (Ker (f *')) holds

(QcFunctional f) . A = f . v

let A be Vector of (VectQuot (V,(Ker (f *')))); :: thesis: for v being Vector of V st A = v + (Ker (f *')) holds

(QcFunctional f) . A = f . v

let v be Vector of V; :: thesis: ( A = v + (Ker (f *')) implies (QcFunctional f) . A = f . v )

assume A1: A = v + (Ker (f *')) ; :: thesis: (QcFunctional f) . A = f . v

the carrier of (Ker (f *')) = ker (f *') by VECTSP10:def 11

.= ker f by Th23 ;

hence (QcFunctional f) . A = f . v by A1, VECTSP10:def 12; :: thesis: verum