let i be Nat; for X, Y being finite natural-membered set st X <N< Y & i < len (Sgm0 Y) holds
(Sgm0 Y) . i = (Sgm0 (X \/ Y)) . (i + (len (Sgm0 X)))
let X, Y be finite natural-membered set ; ( X <N< Y & i < len (Sgm0 Y) implies (Sgm0 Y) . i = (Sgm0 (X \/ Y)) . (i + (len (Sgm0 X))) )
assume that
A1:
X <N< Y
and
A2:
i < len (Sgm0 Y)
; (Sgm0 Y) . i = (Sgm0 (X \/ Y)) . (i + (len (Sgm0 X)))
consider m being Nat such that
A3:
Y c= Segm m
by Th2;
reconsider h = (Sgm0 (X \/ Y)) /^ (len (Sgm0 X)) as XFinSequence of NAT ;
A4:
len (Sgm0 X) = card X
by Th20;
A5:
len (Sgm0 Y) = card Y
by Th20;
then A6:
h . i = (Sgm0 (X \/ Y)) . (i + (card X))
by A1, A2, A4, Th30;
A7:
len (Sgm0 (X \/ Y)) = card (X \/ Y)
by Th20;
X /\ Y =
X /\ (Y /\ NAT)
by A3, XBOOLE_1:1, XBOOLE_1:28
.=
(X /\ Y) /\ NAT
by XBOOLE_1:16
.=
{}
by A1, Th23
;
then
X misses Y
;
then A8:
(card Y) + (card X) = card (X \/ Y)
by CARD_2:40;
len h =
(len (Sgm0 (X \/ Y))) -' (len (Sgm0 X))
by Def2
.=
((card X) + (card Y)) -' (card X)
by A8, A7, Th20
.=
card Y
by NAT_D:34
.=
len (Sgm0 Y)
by Th20
;
then A9:
len h = card Y
by Th20;
A10:
for l, m, k1, k2 being Nat st l < m & m < len h & k1 = h . l & k2 = h . m holds
k1 < k2
proof
let l,
m,
k1,
k2 be
Nat;
( l < m & m < len h & k1 = h . l & k2 = h . m implies k1 < k2 )
assume that A11:
l < m
and A12:
m < len h
and A13:
k1 = h . l
and A14:
k2 = h . m
;
k1 < k2
A15:
m + (card X) < len (Sgm0 (X \/ Y))
by A8, A7, A9, A12, XREAL_1:6;
set m3 =
m + (card X);
set l3 =
l + (card X);
A16:
l + (card X) < m + (card X)
by A11, XREAL_1:6;
l < card Y
by A9, A11, A12, XXREAL_0:2;
then A17:
h . l = (Sgm0 (X \/ Y)) . (l + (card X))
by A1, A4, Th30;
h . m = (Sgm0 (X \/ Y)) . (m + (card X))
by A1, A4, A9, A12, Th30;
hence
k1 < k2
by A13, A14, A17, A15, A16, Def4;
verum
end;
rng h = Y
by A1, A2, A4, A5, Th30;
hence
(Sgm0 Y) . i = (Sgm0 (X \/ Y)) . (i + (len (Sgm0 X)))
by A4, A10, A6, Def4; verum