let K be non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr ; :: thesis: for V, W being VectSp of K
for f being bilinear-Form of V,W holds
( QForm f = RQForm (LQForm f) & QForm f = LQForm (RQForm f) )
let V, W be VectSp of K; :: thesis: for f being bilinear-Form of V,W holds
( QForm f = RQForm (LQForm f) & QForm f = LQForm (RQForm f) )
let f be bilinear-Form of V,W; :: thesis: ( QForm f = RQForm (LQForm f) & QForm f = LQForm (RQForm f) )
set L = LKer f;
set vq = VectQuot (V,(LKer f));
set R = RKer f;
set wq = VectQuot (W,(RKer f));
set RL = RKer (LQForm f);
set wqr = VectQuot (W,(RKer (LQForm f)));
set LR = LKer (RQForm f);
set vql = VectQuot (V,(LKer (RQForm f)));
A1: dom (QForm f) = [: the carrier of (VectQuot (V,(LKer f))), the carrier of (VectQuot (W,(RKer f))):] by FUNCT_2:def 1;

A2: now :: thesis: for x being object st x in dom (QForm f) holds
(QForm f) . x = (RQForm (LQForm f)) . x

let x be object ; :: thesis: ( x in dom (QForm f) implies (QForm f) . x = (RQForm (LQForm f)) . x )
assume x in dom (QForm f) ; :: thesis: (QForm f) . x = (RQForm (LQForm f)) . x
then consider A being Vector of (VectQuot (V,(LKer f))), B being Vector of (VectQuot (W,(RKer f))) such that
A3: x = [A,B] by DOMAIN_1:1;
consider w being Vector of W such that
A4: B = w + (RKer f) by VECTSP10:22;
A5: RKer f = RKer (LQForm f) by Th46;
consider v being Vector of V such that
A6: A = v + (LKer f) by VECTSP10:22;
thus (QForm f) . x = (QForm f) . (A,B) by A3
.= f . (v,w) by A6, A4, Def22
.= (LQForm f) . (A,w) by A6, Def20
.= (RQForm (LQForm f)) . (A,B) by A4, A5, Def21
.= (RQForm (LQForm f)) . x by A3 ; :: thesis: verum

end;

( dom (RQForm (LQForm f)) = [: the carrier of (VectQuot (V,(LKer f))), the carrier of (VectQuot (W,(RKer (LQForm f)))):] & the carrier of (VectQuot (W,(RKer (LQForm f)))) = the carrier of (VectQuot (W,(RKer f))) ) by Th46, FUNCT_2:def 1;
hence QForm f = RQForm (LQForm f) by A1, A2, FUNCT_1:2; :: thesis: QForm f = LQForm (RQForm f)

A7: now :: thesis: for x being object st x in dom (QForm f) holds
(QForm f) . x = (LQForm (RQForm f)) . x

let x be object ; :: thesis: ( x in dom (QForm f) implies (QForm f) . x = (LQForm (RQForm f)) . x )
assume x in dom (QForm f) ; :: thesis: (QForm f) . x = (LQForm (RQForm f)) . x
then consider A being Vector of (VectQuot (V,(LKer f))), B being Vector of (VectQuot (W,(RKer f))) such that
A8: x = [A,B] by DOMAIN_1:1;
consider w being Vector of W such that
A9: B = w + (RKer f) by VECTSP10:22;
A10: LKer f = LKer (RQForm f) by Th47;
consider v being Vector of V such that
A11: A = v + (LKer f) by VECTSP10:22;
thus (QForm f) . x = (QForm f) . (A,B) by A8
.= f . (v,w) by A11, A9, Def22
.= (RQForm f) . (v,B) by A9, Def21
.= (LQForm (RQForm f)) . (A,B) by A11, A10, Def20
.= (LQForm (RQForm f)) . x by A8 ; :: thesis: verum

end;

( dom (LQForm (RQForm f)) = [: the carrier of (VectQuot (V,(LKer (RQForm f)))), the carrier of (VectQuot (W,(RKer f))):] & the carrier of (VectQuot (V,(LKer (RQForm f)))) = the carrier of (VectQuot (V,(LKer f))) ) by Th47, FUNCT_2:def 1;
hence QForm f = LQForm (RQForm f) by A1, A7, FUNCT_1:2; :: thesis: verum