let i be Nat; for X, Y being finite natural-membered set st X <N< Y & i < len (Sgm0 X) holds
(Sgm0 X) . i = (Sgm0 (X \/ Y)) . i
let X, Y be finite natural-membered set ; ( X <N< Y & i < len (Sgm0 X) implies (Sgm0 X) . i = (Sgm0 (X \/ Y)) . i )
assume that
A1:
X <N< Y
and
A2:
i < len (Sgm0 X)
; (Sgm0 X) . i = (Sgm0 (X \/ Y)) . i
reconsider h = (Sgm0 (X \/ Y)) | (len (Sgm0 X)) as XFinSequence of NAT ;
A3:
len (Sgm0 X) = card X
by Th20;
then A4:
h . i = (Sgm0 (X \/ Y)) . i
by A1, A2, Th27;
Segm (card X) c= Segm (card (X \/ Y))
by CARD_1:11, XBOOLE_1:7;
then A5:
card X <= card (X \/ Y)
by NAT_1:39;
then
card X <= len (Sgm0 (X \/ Y))
by Th20;
then A6:
len (Sgm0 X) <= len (Sgm0 (X \/ Y))
by Th20;
A7:
len (Sgm0 (X \/ Y)) = card (X \/ Y)
by Th20;
then A8:
len h = len (Sgm0 X)
by A5, A3, AFINSQ_1:54;
A9:
len h = card X
by A5, A3, A7, AFINSQ_1:54;
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 < len (Sgm0 (X \/ Y))
by A8, A6, A12, XXREAL_0:2;
l < card X
by A9, A11, A12, XXREAL_0:2;
then A16:
h . l = (Sgm0 (X \/ Y)) . l
by A1, A3, Th27;
h . m = (Sgm0 (X \/ Y)) . m
by A1, A3, A8, A12, Th27;
hence
k1 < k2
by A11, A13, A14, A16, A15, Def4;
verum
end;
rng h = X
by A1, A2, A3, Th27;
hence
(Sgm0 X) . i = (Sgm0 (X \/ Y)) . i
by A10, A4, Def4; verum