set K = F_Complex ;
let V, W be VectSp of F_Complex ; 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; ( 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 for x being object st x in dom (Q*Form f) holds
(Q*Form f) . x = (RQ*Form (LQForm f)) . xA3:
RKer (f *') = RKer ((LQForm f) *')
by Th61;
let x be
object ;
( x in dom (Q*Form f) implies (Q*Form f) . x = (RQ*Form (LQForm f)) . x )assume
x in dom (Q*Form f)
;
(Q*Form f) . x = (RQ*Form (LQForm f)) . xthen 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
;
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; Q*Form f = LQForm (RQ*Form f)
A9:
now for x being object st x in dom (Q*Form f) holds
(Q*Form f) . x = (LQForm (RQ*Form f)) . xA10:
LKer f = LKer (RQ*Form f)
by Th62;
let x be
object ;
( x in dom (Q*Form f) implies (Q*Form f) . x = (LQForm (RQ*Form f)) . x )assume
x in dom (Q*Form f)
;
(Q*Form f) . x = (LQForm (RQ*Form f)) . xthen 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
;
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; verum