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 Th26 ;
hence (QcFunctional f) . A = f . v by A1, VECTSP10:def 12; :: thesis: verum