let K be non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr ; :: thesis: for V being VectSp of K
for f being linear-Functional of V
for A being Vector of (VectQuot (V,(Ker f)))
for v being Vector of V st A = v + (Ker f) holds
(CQFunctional f) . A = f . v
let V be VectSp of K; :: thesis: for f being linear-Functional of V
for A being Vector of (VectQuot (V,(Ker f)))
for v being Vector of V st A = v + (Ker f) holds
(CQFunctional f) . A = f . v
let f be linear-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
(CQFunctional 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
(CQFunctional f) . A = f . v
let v be Vector of V; :: thesis: ( A = v + (Ker f) implies (CQFunctional f) . A = f . v )
assume A1: A = v + (Ker f) ; :: thesis: (CQFunctional f) . A = f . v
the carrier of (Ker f) = ker f by Def11;
hence (CQFunctional f) . A = f . v by A1, Def12; :: thesis: verum