let D be non empty set ; for A being Matrix of D
for P, P1, P2, Q, Q1, Q2 being finite without_zero Subset of NAT st P c= P1 & Q c= Q1 & P2 = (Sgm P1) " P & Q2 = (Sgm Q1) " Q holds
( [:(rng (Sgm P2)),(rng (Sgm Q2)):] c= Indices (Segm (A,P1,Q1)) & Segm ((Segm (A,P1,Q1)),P2,Q2) = Segm (A,P,Q) )
let A be Matrix of D; for P, P1, P2, Q, Q1, Q2 being finite without_zero Subset of NAT st P c= P1 & Q c= Q1 & P2 = (Sgm P1) " P & Q2 = (Sgm Q1) " Q holds
( [:(rng (Sgm P2)),(rng (Sgm Q2)):] c= Indices (Segm (A,P1,Q1)) & Segm ((Segm (A,P1,Q1)),P2,Q2) = Segm (A,P,Q) )
let P, P1, P2, Q, Q1, Q2 be finite without_zero Subset of NAT; ( P c= P1 & Q c= Q1 & P2 = (Sgm P1) " P & Q2 = (Sgm Q1) " Q implies ( [:(rng (Sgm P2)),(rng (Sgm Q2)):] c= Indices (Segm (A,P1,Q1)) & Segm ((Segm (A,P1,Q1)),P2,Q2) = Segm (A,P,Q) ) )
assume that
A1:
P c= P1
and
A2:
Q c= Q1
and
A3:
P2 = (Sgm P1) " P
and
A4:
Q2 = (Sgm Q1) " Q
; ( [:(rng (Sgm P2)),(rng (Sgm Q2)):] c= Indices (Segm (A,P1,Q1)) & Segm ((Segm (A,P1,Q1)),P2,Q2) = Segm (A,P,Q) )
set SA = Segm (A,P1,Q1);
A5:
card Q = card Q2
by A2, A4, Lm2;
card P = card P2
by A1, A3, Lm2;
then reconsider SAA = Segm ((Segm (A,P1,Q1)),P2,Q2) as Matrix of card P, card Q,D by A5;
set Sq2 = Sgm Q2;
set Sp2 = Sgm P2;
set Sq1 = Sgm Q1;
set Sp1 = Sgm P1;
set S = Segm (A,P,Q);
A6:
ex q2 being Nat st Q2 c= Seg q2
by Th43;
then A7:
rng (Sgm Q2) = Q2
by FINSEQ_1:def 13;
A8:
ex p2 being Nat st P2 c= Seg p2
by Th43;
then
rng (Sgm P2) = P2
by FINSEQ_1:def 13;
hence A9:
[:(rng (Sgm P2)),(rng (Sgm Q2)):] c= Indices (Segm (A,P1,Q1))
by A3, A4, A7, Th55; Segm ((Segm (A,P1,Q1)),P2,Q2) = Segm (A,P,Q)
now for i, j being Nat st [i,j] in Indices (Segm (A,P,Q)) holds
(Segm (A,P,Q)) * (i,j) = SAA * (i,j)A10:
(Sgm Q1) * (Sgm Q2) = Sgm Q
by A2, A4, Th54;
let i,
j be
Nat;
( [i,j] in Indices (Segm (A,P,Q)) implies (Segm (A,P,Q)) * (i,j) = SAA * (i,j) )assume A11:
[i,j] in Indices (Segm (A,P,Q))
;
(Segm (A,P,Q)) * (i,j) = SAA * (i,j)A12:
[i,j] in Indices SAA
by A11, MATRIX_0:26;
then A13:
j in Seg (width SAA)
by ZFMISC_1:87;
reconsider Sp2i =
(Sgm P2) . i,
Sq2j =
(Sgm Q2) . j as
Element of
NAT by ORDINAL1:def 12;
A14:
(Sgm P1) * (Sgm P2) = Sgm P
by A1, A3, Th54;
Indices SAA = [:(Seg (card P2)),(Seg (width SAA)):]
by MATRIX_0:25;
then A15:
i in Seg (card P2)
by A12, ZFMISC_1:87;
then
card P2 <> 0
;
then
width SAA = card Q2
by Th1;
then
j in dom (Sgm Q2)
by A6, A13, FINSEQ_3:40;
then A16:
(Sgm Q1) . Sq2j = (Sgm Q) . j
by A10, FUNCT_1:13;
reconsider i9 =
i,
j9 =
j as
Element of
NAT by ORDINAL1:def 12;
A17:
[i9,j9] in Indices SAA
by A11, MATRIX_0:26;
then A18:
SAA * (
i,
j)
= (Segm (A,P1,Q1)) * (
Sp2i,
Sq2j)
by Def1;
i in dom (Sgm P2)
by A8, A15, FINSEQ_3:40;
then A19:
(Sgm P1) . Sp2i = (Sgm P) . i
by A14, FUNCT_1:13;
[Sp2i,Sq2j] in Indices (Segm (A,P1,Q1))
by A9, A17, Th17;
then
SAA * (
i,
j)
= A * (
((Sgm P1) . Sp2i),
((Sgm Q1) . Sq2j))
by A18, Def1;
hence
(Segm (A,P,Q)) * (
i,
j)
= SAA * (
i,
j)
by A11, A19, A16, Def1;
verum end;
hence
Segm ((Segm (A,P1,Q1)),P2,Q2) = Segm (A,P,Q)
by MATRIX_0:27; verum