let K be non empty right_complementable almost_left_invertible Abelian add-associative right_zeroed well-unital distributive associative commutative doubleLoopStr ; :: thesis:
let V be VectSp of K; :: thesis:
let W be non empty ModuleStr over K; :: thesis:
let f be linear-Functional of V; :: thesis:
let g be Functional of W; :: thesis:
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:
then A1: leftker (FormFunctional (f,g)) = ker f by Th51;
the carrier of (LKer (FormFunctional (f,g))) = leftker (FormFunctional (f,g)) by Def18;
hence A2: LKer (FormFunctional (f,g)) = Ker f by A1, VECTSP10:def 11; :: thesis:

A3: now :: thesis:

let x be object ; :: thesis:
assume x in dom (FormFunctional ((CQFunctional f),g)) ; :: thesis:
then consider A being Vector of (VectQuot (V,(Ker f))), B being Vector of W such that
A4: x = [A,B] by DOMAIN_1:1;
consider v being Vector of V such that
A5: A = v + (Ker f) by VECTSP10:22;
thus (FormFunctional ((CQFunctional f),g)) . x = (FormFunctional ((CQFunctional f),g)) . (A,B) by A4
.= ((CQFunctional f) . A) * (g . B) by Def10
.= (f . v) * (g . B) by A5, VECTSP10:35
.= (FormFunctional (f,g)) . (v,B) by Def10
.= (LQForm (FormFunctional (f,g))) . (A,B) by A2, A5, Def20
.= (LQForm (FormFunctional (f,g))) . x by A4 ; :: thesis:

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:2; :: thesis: