let i be Nat; :: thesis: 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 ; :: thesis: ( 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) ; :: thesis: (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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: 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; :: thesis: verum