let K be non empty right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ; :: thesis:
let V be VectSp of K; :: thesis:
let W be non empty VectSpStr of K; :: thesis:
let f be linear-Functional of V; :: thesis:
let g be Functional of W; :: thesis:
assume A1: g <> 0Functional 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);
A2: the carrier of (LKer (FormFunctional f,g)) = leftker (FormFunctional f,g) by Def19;
leftker (FormFunctional f,g) = ker f by A1, Th52;
hence A3: LKer (FormFunctional f,g) = Ker f by A2, VECTSP10:def 11; :: thesis:
A4: dom (LQForm (FormFunctional f,g)) = [:the carrier of (VectQuot V,(LKer (FormFunctional f,g))),the carrier of W:] by FUNCT_2:def 1;
A5: dom (FormFunctional (CQFunctional f),g) = [:the carrier of (VectQuot V,(Ker f)),the carrier of W:] by FUNCT_2:def 1;

now

let x be set ; :: 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
A6: x = [A,B] by DOMAIN_1:9;
consider v being Vector of V such that
A7: A = v + (Ker f) by VECTSP10:23;
thus (FormFunctional (CQFunctional f),g) . x = (FormFunctional (CQFunctional f),g) . A,B by A6
.= ((CQFunctional f) . A) * (g . B) by Def11
.= (f . v) * (g . B) by A7, VECTSP10:36
.= (FormFunctional f,g) . v,B by Def11
.= (LQForm (FormFunctional f,g)) . A,B by A3, A7, Def21
.= (LQForm (FormFunctional f,g)) . x by A6 ; :: thesis:

end;

hence LQForm (FormFunctional f,g) = FormFunctional (CQFunctional f),g by A3, A4, A5, FUNCT_1:9; :: thesis: