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 A3:
RKer (f *' ) = RKer ((LQForm f) *' )
by Th64;
let x be
set ;
( 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
set 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:23;
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:23;
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 21
.=
(RQ*Form (LQForm f)) . A,
B
by A8, A3, Th62
.=
(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 Th64, FUNCT_2:def 1;
hence
Q*Form f = RQ*Form (LQForm f)
by A1, A2, FUNCT_1:9; Q*Form f = LQForm (RQ*Form f)
A9:
now A10:
LKer f = LKer (RQ*Form f)
by Th65;
let x be
set ;
( 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
set 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:23;
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:23;
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, Th62
.=
(LQForm (RQ*Form f)) . A,
B
by A14, A10, BILINEAR:def 21
.=
(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 Th65, FUNCT_2:def 1;
hence
Q*Form f = LQForm (RQ*Form f)
by A1, A9, FUNCT_1:9; verum