let K be non empty right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ; :: thesis: for V being VectSp of K
for W being non empty VectSpStr of K
for f being linear-Functional of V
for g being Functional of W st g <> 0Functional W holds
( LKer (FormFunctional f,g) = Ker f & LQForm (FormFunctional f,g) = FormFunctional (CQFunctional f),g )
let V be VectSp of K; :: thesis: for W being non empty VectSpStr of K
for f being linear-Functional of V
for g being Functional of W st g <> 0Functional W holds
( LKer (FormFunctional f,g) = Ker f & LQForm (FormFunctional f,g) = FormFunctional (CQFunctional f),g )
let W be non empty VectSpStr of K; :: thesis: for f being linear-Functional of V
for g being Functional of W st g <> 0Functional W holds
( LKer (FormFunctional f,g) = Ker f & LQForm (FormFunctional f,g) = FormFunctional (CQFunctional f),g )
let f be linear-Functional of V; :: thesis: for g being Functional of W st g <> 0Functional W holds
( LKer (FormFunctional f,g) = Ker f & LQForm (FormFunctional f,g) = FormFunctional (CQFunctional f),g )
let g be Functional of W; :: thesis: ( g <> 0Functional W implies ( LKer (FormFunctional f,g) = Ker f & LQForm (FormFunctional f,g) = FormFunctional (CQFunctional f),g ) )
set fg = FormFunctional f,g;
set cf = CQFunctional f;
set fcfg = FormFunctional (CQFunctional f),g;
set vql = VectQuot V,(LKer (FormFunctional f,g));
set vq = VectQuot V,(Ker f);
assume g <> 0Functional W ; :: thesis: ( LKer (FormFunctional f,g) = Ker f & LQForm (FormFunctional f,g) = FormFunctional (CQFunctional f),g )
then A1: leftker (FormFunctional f,g) = ker f by Th52;
the carrier of (LKer (FormFunctional f,g)) = leftker (FormFunctional f,g) by Def19;
hence A2: LKer (FormFunctional f,g) = Ker f by A1, VECTSP10:def 11; :: thesis: LQForm (FormFunctional f,g) = FormFunctional (CQFunctional f),g

A3: now

let x be set ; :: thesis: ( x in dom (FormFunctional (CQFunctional f),g) implies (FormFunctional (CQFunctional f),g) . x = (LQForm (FormFunctional f,g)) . x )
assume x in dom (FormFunctional (CQFunctional f),g) ; :: thesis: (FormFunctional (CQFunctional f),g) . x = (LQForm (FormFunctional f,g)) . x
then consider A being Vector of (VectQuot V,(Ker f)), B being Vector of W such that
A4: x = [A,B] by DOMAIN_1:9;
consider v being Vector of V such that
A5: A = v + (Ker f) by VECTSP10:23;
thus (FormFunctional (CQFunctional f),g) . x = (FormFunctional (CQFunctional f),g) . A,B by A4
.= ((CQFunctional f) . A) * (g . B) by Def11
.= (f . v) * (g . B) by A5, VECTSP10:36
.= (FormFunctional f,g) . v,B by Def11
.= (LQForm (FormFunctional f,g)) . A,B by A2, A5, Def21
.= (LQForm (FormFunctional f,g)) . x by A4 ; :: thesis: verum

end;

( dom (LQForm (FormFunctional f,g)) = [:the carrier of (VectQuot V,(LKer (FormFunctional f,g))),the carrier of W:] & dom (FormFunctional (CQFunctional f),g) = [:the carrier of (VectQuot V,(Ker f)),the carrier of W:] ) by FUNCT_2:def 1;
hence LQForm (FormFunctional f,g) = FormFunctional (CQFunctional f),g by A2, A3, FUNCT_1:9; :: thesis: verum