set K = F_Complex ;
let V, W be VectSp of F_Complex ; :: thesis: for f being sesquilinear-Form of V,W holds
( Q*Form f = RQ*Form (LQForm f) & Q*Form f = LQForm (RQ*Form f) )
let f be sesquilinear-Form of V,W; :: thesis: ( Q*Form f = RQ*Form (LQForm f) & Q*Form f = LQForm (RQ*Form 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 (RQ*Form f);
set vql = VectQuot (V,(LKer (RQ*Form f)));
A1: dom (Q*Form 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 (Q*Form f) holds
(Q*Form f) . x = (RQ*Form (LQForm f)) . x

A3: RKer (f *') = RKer ((LQForm f) *') by Th61;
let x be object ; :: thesis: ( x in dom (Q*Form f) implies (Q*Form f) . x = (RQ*Form (LQForm f)) . x )
assume x in dom (Q*Form f) ; :: thesis: (Q*Form f) . x = (RQ*Form (LQForm f)) . x
then consider A, B being object such that
A4: A in the carrier of (VectQuot (V,(LKer f))) and
A5: B in the carrier of (VectQuot (W,(RKer (f *')))) and
A6: x = [A,B] by ZFMISC_1:def 2;
reconsider A = A as Vector of (VectQuot (V,(LKer f))) by A4;
consider v being Vector of V such that
A7: A = v + (LKer f) by VECTSP10:22;
reconsider B = B as Vector of (VectQuot (W,(RKer (f *')))) by A5;
consider w being Vector of W such that
A8: B = w + (RKer (f *')) by VECTSP10:22;
thus (Q*Form f) . x = (Q*Form f) . (A,B) by A6
.= f . (v,w) by A7, A8, Def12
.= (LQForm f) . (A,w) by A7, BILINEAR:def 20
.= (RQ*Form (LQForm f)) . (A,B) by A8, A3, Th59
.= (RQ*Form (LQForm f)) . x by A6 ; :: thesis: verum

end;

( dom (RQ*Form (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 Th61, FUNCT_2:def 1;
hence Q*Form f = RQ*Form (LQForm f) by A1, A2; :: thesis: Q*Form f = LQForm (RQ*Form f)

A9: now :: thesis: for x being object st x in dom (Q*Form f) holds
(Q*Form f) . x = (LQForm (RQ*Form f)) . x

A10: LKer f = LKer (RQ*Form f) by Th62;
let x be object ; :: thesis: ( x in dom (Q*Form f) implies (Q*Form f) . x = (LQForm (RQ*Form f)) . x )
assume x in dom (Q*Form f) ; :: thesis: (Q*Form f) . x = (LQForm (RQ*Form f)) . x
then consider A, B being object such that
A11: A in the carrier of (VectQuot (V,(LKer f))) and
A12: B in the carrier of (VectQuot (W,(RKer (f *')))) and
A13: x = [A,B] by ZFMISC_1:def 2;
reconsider A = A as Vector of (VectQuot (V,(LKer f))) by A11;
consider v being Vector of V such that
A14: A = v + (LKer f) by VECTSP10:22;
reconsider B = B as Vector of (VectQuot (W,(RKer (f *')))) by A12;
consider w being Vector of W such that
A15: B = w + (RKer (f *')) by VECTSP10:22;
thus (Q*Form f) . x = (Q*Form f) . (A,B) by A13
.= f . (v,w) by A14, A15, Def12
.= (RQ*Form f) . (v,B) by A15, Th59
.= (LQForm (RQ*Form f)) . (A,B) by A14, A10, BILINEAR:def 20
.= (LQForm (RQ*Form f)) . x by A13 ; :: thesis: verum

end;

( dom (LQForm (RQ*Form f)) = [: the carrier of (VectQuot (V,(LKer (RQ*Form f)))), the carrier of (VectQuot (W,(RKer (f *')))):] & the carrier of (VectQuot (V,(LKer (RQ*Form f)))) = the carrier of (VectQuot (V,(LKer f))) ) by Th62, FUNCT_2:def 1;
hence Q*Form f = LQForm (RQ*Form f) by A1, A9; :: thesis: verum