let X, Y be finite natural-membered set ; :: thesis: for i being Nat st X <N< Y & i in card X holds
(Sgm0 (X \/ Y)) . i in X
let i be Nat; :: thesis: ( X <N< Y & i in card X implies (Sgm0 (X \/ Y)) . i in X )
assume A1: ( X <N< Y & i in card X ) ; :: thesis: (Sgm0 (X \/ Y)) . i in X
A20: X \/ Y <> {} by A1, CARD_1:47, XBOOLE_1:15;
set f0 = Sgm0 (X \/ Y);
A30: rng (Sgm0 (X \/ Y)) = X \/ Y by AC113;
set f = (Sgm0 (X \/ Y)) | (card X);
set Z = { v where v is Element of X \/ Y : ex k2 being Nat st
( v = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) } ;
A33: len (Sgm0 (X \/ Y)) = card (X \/ Y) by Th44;
A22: card X <= len (Sgm0 (X \/ Y)) by A33, NAT_1:44, XBOOLE_1:7;
then A4: len ((Sgm0 (X \/ Y)) | (card X)) = card X by TH80;
B4: rng ((Sgm0 (X \/ Y)) | (card X)) c= rng (Sgm0 (X \/ Y)) by RELAT_1:99;
A3: rng ((Sgm0 (X \/ Y)) | (card X)) c= { v where v is Element of X \/ Y : ex k2 being Nat st
( v = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) }

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((Sgm0 (X \/ Y)) | (card X)) or y in { v where v is Element of X \/ Y : ex k2 being Nat st
( v = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) } )
assume B1: y in rng ((Sgm0 (X \/ Y)) | (card X)) ; :: thesis: y in { v where v is Element of X \/ Y : ex k2 being Nat st
( v = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) }
then consider x being set such that
B2: ( x in dom ((Sgm0 (X \/ Y)) | (card X)) & y = ((Sgm0 (X \/ Y)) | (card X)) . x ) by FUNCT_1:def 5;
reconsider nx = x as Nat by B2;
reconsider y0 = y as Element of X \/ Y by B1, B4, AC113;
ex k2 being Nat st
( y0 = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) by A4, B2;
hence y in { v where v is Element of X \/ Y : ex k2 being Nat st
( v = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) } ; :: thesis: verum

end;

{ v where v is Element of X \/ Y : ex k2 being Nat st
( v = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) } c= rng ((Sgm0 (X \/ Y)) | (card X))

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in { v where v is Element of X \/ Y : ex k2 being Nat st
( v = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) } or y in rng ((Sgm0 (X \/ Y)) | (card X)) )
assume y in { v where v is Element of X \/ Y : ex k2 being Nat st
( v = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) } ; :: thesis: y in rng ((Sgm0 (X \/ Y)) | (card X))
then consider v0 being Element of X \/ Y such that
B2: ( y = v0 & ex k2 being Nat st
( v0 = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) ) ;
thus y in rng ((Sgm0 (X \/ Y)) | (card X)) by B2, A4, FUNCT_1:def 5; :: thesis: verum

end;

then A40: rng ((Sgm0 (X \/ Y)) | (card X)) = { v where v is Element of X \/ Y : ex k2 being Nat st
( v = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) } by A3, XBOOLE_0:def 10;

A50n: now

assume B1: ( not { v where v is Element of X \/ Y : ex k2 being Nat st
( v = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) } c= X & not X c= { v where v is Element of X \/ Y : ex k2 being Nat st
( v = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) } ) ; :: thesis: contradiction
then consider v1 being set such that
B2: ( v1 in { v where v is Element of X \/ Y : ex k2 being Nat st
( v = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) } & not v1 in X ) by TARSKI:def 3;
consider v2 being set such that
B3: ( v2 in X & not v2 in { v where v is Element of X \/ Y : ex k2 being Nat st
( v = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) } ) by B1, TARSKI:def 3;
consider v10 being Element of X \/ Y such that
B4: ( v1 = v10 & ex k2 being Nat st
( v10 = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) ) by B2;
B98: v10 in Y by A20, B2, B4, XBOOLE_0:def 3;
consider k20 being Nat such that
B4b: ( v10 = ((Sgm0 (X \/ Y)) | (card X)) . k20 & k20 in card X ) by B4;
reconsider nv10 = v10 as Nat ;
X c= X \/ Y by XBOOLE_1:7;
then consider x2 being set such that
B5: ( x2 in dom (Sgm0 (X \/ Y)) & v2 = (Sgm0 (X \/ Y)) . x2 ) by B3, A30, FUNCT_1:def 5;
reconsider x20 = x2 as Nat by B5;
reconsider nv2 = v2 as Nat by B5;

now

assume C0: x20 < card X ; :: thesis: contradiction
card X <= card (X \/ Y) by NAT_1:44, XBOOLE_1:7;
then C4: ( card X <= len (Sgm0 (X \/ Y)) & x20 in card X ) by C0, Th44, NAT_1:45;
then ((Sgm0 (X \/ Y)) | (card X)) . x20 = (Sgm0 (X \/ Y)) . x20 by Th19;
hence contradiction by B3, B5, A40, C4, A4, FUNCT_1:def 5; :: thesis: verum

end;

then B61: len ((Sgm0 (X \/ Y)) | (card X)) <= x20 by TH80, A22;
k20 < len ((Sgm0 (X \/ Y)) | (card X)) by B4b, A4, NAT_1:45;
then B62: k20 < x20 by B61, XXREAL_0:2;
B44: ((Sgm0 (X \/ Y)) | (card X)) . k20 = (Sgm0 (X \/ Y)) . k20 by Th19, A22, B4b;
x20 < len (Sgm0 (X \/ Y)) by B5, NAT_1:45;
then nv10 < nv2 by B4b, B5, AC113, B62, B44;
hence contradiction by AE100, A1, B3, B98; :: thesis: verum

end;

(Sgm0 (X \/ Y)) | (card X) is one-to-one by FUNCT_1:84;
then A51: dom ((Sgm0 (X \/ Y)) | (card X)),((Sgm0 (X \/ Y)) | (card X)) .: (dom ((Sgm0 (X \/ Y)) | (card X))) are_equipotent by CARD_1:60;
((Sgm0 (X \/ Y)) | (card X)) .: (dom ((Sgm0 (X \/ Y)) | (card X))) = rng ((Sgm0 (X \/ Y)) | (card X)) by RELAT_1:146;
then ak: card { v where v is Element of X \/ Y : ex k2 being Nat st
( v = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) } = card (len ((Sgm0 (X \/ Y)) | (card X))) by A40, A51, CARD_1:21;
then A53: card { v where v is Element of X \/ Y : ex k2 being Nat st
( v = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) } = card X by TH80, A22;
then X,{ v where v is Element of X \/ Y : ex k2 being Nat st
( v = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) } are_equipotent by CARD_1:21;
then reconsider Z0 = { v where v is Element of X \/ Y : ex k2 being Nat st
( v = ((Sgm0 (X \/ Y)) | (card X)) . k2 & k2 in card X ) } as finite set by CARD_1:68;

A77n: now

per cases ( Z0 c= X or X c= Z0 ) by A50n;

case Z0 c= X ; :: thesis: Z0 = X

hence Z0 = X by ak, TH80, A22, CARD_FIN:1; :: thesis: verum

end;

case X c= Z0 ; :: thesis: Z0 = X

hence Z0 = X by A53, CARD_FIN:1; :: thesis: verum

end;

end;

end;

((Sgm0 (X \/ Y)) | (card X)) . i = (Sgm0 (X \/ Y)) . i by Th19, A22, A1;
hence (Sgm0 (X \/ Y)) . i in X by A77n, A40, A1, A4, FUNCT_1:def 5; :: thesis: verum