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 non empty ModuleStr over K; :: thesis:
let W be VectSp of K; :: thesis:
let f be Functional of V; :: thesis:
let g be linear-Functional of W; :: thesis:
set fg = FormFunctional (f,g);
set cg = CQFunctional g;
set fcfg = FormFunctional (f,(CQFunctional g));
set wqr = VectQuot (W,(RKer (FormFunctional (f,g))));
set wq = VectQuot (W,(Ker g));
assume f <> 0Functional V ; :: thesis:
then A1: rightker (FormFunctional (f,g)) = ker g by Th53;
the carrier of (RKer (FormFunctional (f,g))) = rightker (FormFunctional (f,g)) by Def19;
hence A2: RKer (FormFunctional (f,g)) = Ker g by A1, VECTSP10:def 11; :: thesis:

A3: now :: thesis:

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

end;

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