let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive 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

let x be set ; :: 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:9;
consider w being Vector of W such that
A4: B = w + (RKer f) by VECTSP10:23;
A5: RKer f = RKer (LQForm f) by Th47;
consider v being Vector of V such that
A6: A = v + (LKer f) by VECTSP10:23;
thus (QForm f) . x = (QForm f) . A,B by A3
.= f . v,w by A6, A4, Def23
.= (LQForm f) . A,w by A6, Def21
.= (RQForm (LQForm f)) . A,B by A4, A5, Def22
.= (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 Th47, FUNCT_2:def 1;
hence QForm f = RQForm (LQForm f) by A1, A2, FUNCT_1:9; :: thesis: QForm f = LQForm (RQForm f)

A7: now

let x be set ; :: 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:9;
consider w being Vector of W such that
A9: B = w + (RKer f) by VECTSP10:23;
A10: LKer f = LKer (RQForm f) by Th48;
consider v being Vector of V such that
A11: A = v + (LKer f) by VECTSP10:23;
thus (QForm f) . x = (QForm f) . A,B by A8
.= f . v,w by A11, A9, Def23
.= (RQForm f) . v,B by A9, Def22
.= (LQForm (RQForm f)) . A,B by A11, A10, Def21
.= (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 Th48, FUNCT_2:def 1;
hence QForm f = LQForm (RQForm f) by A1, A7, FUNCT_1:9; :: thesis: verum