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

end;

rng h = X by A1, A2, A3, Th27;
hence (Sgm0 X) . i = (Sgm0 (X \/ Y)) . i by A10, A4, Def4; :: thesis: verum