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;

hence QForm f = RQForm (LQForm f) by A1, A2, FUNCT_1:2; :: thesis: QForm f = LQForm (RQForm f)

hence QForm f = LQForm (RQForm f) by A1, A7, FUNCT_1:2; :: thesis: verum

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

( 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;(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;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

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

( 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;(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;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

hence QForm f = LQForm (RQForm f) by A1, A7, FUNCT_1:2; :: thesis: verum