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;

hence Q*Form f = RQ*Form (LQForm f) by A1, A2; :: thesis: Q*Form f = LQForm (RQ*Form f)

hence Q*Form f = LQForm (RQ*Form f) by A1, A9; :: thesis: verum

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

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

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

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

hence Q*Form f = LQForm (RQ*Form f) by A1, A9; :: thesis: verum