let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; :: thesis: for V being VectSp of
for f being linear-Functional of V
for A being Vector of
for v being Vector of st A = v + (Ker f) holds
(CQFunctional f) . A = f . v
let V be VectSp of ; :: thesis: for f being linear-Functional of V
for A being Vector of
for v being Vector of st A = v + (Ker f) holds
(CQFunctional f) . A = f . v
let f be linear-Functional of V; :: thesis: for A being Vector of
for v being Vector of st A = v + (Ker f) holds
(CQFunctional f) . A = f . v
let A be Vector of ; :: thesis: for v being Vector of st A = v + (Ker f) holds
(CQFunctional f) . A = f . v
let v be Vector of ; :: 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