let X, Y be finite natural-membered set ; :: thesis: for i being Nat st X <N< Y & i < len (Sgm0 X) holds
(Sgm0 X) . i = (Sgm0 (X \/ Y)) . i
let i be Nat; :: thesis: ( X <N< Y & i < len (Sgm0 X) implies (Sgm0 X) . i = (Sgm0 (X \/ Y)) . i )
assume A1: ( X <N< Y & i < len (Sgm0 X) ) ; :: thesis: (Sgm0 X) . i = (Sgm0 (X \/ Y)) . i
card X c= card (X \/ Y) by CARD_1:27, XBOOLE_1:7;
then A102: card X <= card (X \/ Y) by NAT_1:40;
A56: len (Sgm0 X) = card X by Th44;
reconsider h = (Sgm0 (X \/ Y)) | (len (Sgm0 X)) as XFinSequence of ;
A230bn: len (Sgm0 (X \/ Y)) = card (X \/ Y) by Th44;
then A230b: len h = len (Sgm0 X) by TH80, A102, A56;
A230: len h = card X by TH80, A102, A56, A230bn;
card X <= len (Sgm0 (X \/ Y)) by A102, Th44;
then A101: len (Sgm0 X) <= len (Sgm0 (X \/ Y)) by Th44;
A100: 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 B1: ( l < m & m < len h & k1 = h . l & k2 = h . m ) ; :: thesis: k1 < k2
l < card X by B1, A230, XXREAL_0:2;
then B3: h . l = (Sgm0 (X \/ Y)) . l by A1, AE221e, A56;
B4: h . m = (Sgm0 (X \/ Y)) . m by A1, AE221e, B1, A56, A230b;
m < len (Sgm0 (X \/ Y)) by B1, A230b, A101, XXREAL_0:2;
hence k1 < k2 by B3, B4, AC113, B1; :: thesis: verum

end;

A103: rng h = X by A1, AE221e, A56;
h . i = (Sgm0 (X \/ Y)) . i by A1, AE221e, A56;
hence (Sgm0 X) . i = (Sgm0 (X \/ Y)) . i by AC113, A100, A103; :: thesis: verum