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 non empty VectSpStr of 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 Th54;
the carrier of (RKer (FormFunctional f,g)) = rightker (FormFunctional f,g) by Def20;
hence A2: RKer (FormFunctional f,g) = Ker g by A1, VECTSP10:def 11; :: thesis:

A3: now

let x be set ; :: 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:9;
consider w being Vector of W such that
A5: B = w + (Ker g) by VECTSP10:23;
thus (FormFunctional f,(CQFunctional g)) . x = (FormFunctional f,(CQFunctional g)) . A,B by A4
.= (f . A) * ((CQFunctional g) . B) by Def11
.= (f . A) * (g . w) by A5, VECTSP10:36
.= (FormFunctional f,g) . A,w by Def11
.= (RQForm (FormFunctional f,g)) . A,B by A2, A5, Def22
.= (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:9; :: thesis: