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