let X0, Y0 be finite natural-membered set ; :: thesis: for i being Nat st X0 <N< Y0 & i < card Y0 holds
( rng ((Sgm0 (X0 \/ Y0)) /^ (card X0)) = Y0 & ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . i = (Sgm0 (X0 \/ Y0)) . (i + (card X0)) )
let i be Nat; :: thesis: ( X0 <N< Y0 & i < card Y0 implies ( rng ((Sgm0 (X0 \/ Y0)) /^ (card X0)) = Y0 & ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . i = (Sgm0 (X0 \/ Y0)) . (i + (card X0)) ) )
assume A1: ( X0 <N< Y0 & i < card Y0 ) ; :: thesis: ( rng ((Sgm0 (X0 \/ Y0)) /^ (card X0)) = Y0 & ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . i = (Sgm0 (X0 \/ Y0)) . (i + (card X0)) )
consider n being Nat such that
A1d: Y0 c= n by AE221f;
A1e: n c= NAT by MEMBERED:6;
A20: X0 \/ Y0 <> {} by A1, CARD_1:47, XBOOLE_1:15;
set f0 = Sgm0 (X0 \/ Y0);
A30: rng (Sgm0 (X0 \/ Y0)) = X0 \/ Y0 by AC113;
set f = (Sgm0 (X0 \/ Y0)) /^ (card X0);
set Z = { v where v is Element of X0 \/ Y0 : ex k2 being Nat st
( v = ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . k2 & k2 in card Y0 ) } ;
A33: len (Sgm0 (X0 \/ Y0)) = card (X0 \/ Y0) by Th44;
A22: card X0 <= len (Sgm0 (X0 \/ Y0)) by A33, NAT_1:44, XBOOLE_1:7;
A74: len ((Sgm0 (X0 \/ Y0)) /^ (card X0)) = (len (Sgm0 (X0 \/ Y0))) -' (card X0) by Def2
.= (len (Sgm0 (X0 \/ Y0))) - (card X0) by A22, XREAL_1:235 ;
X0 /\ Y0 = X0 /\ (Y0 /\ NAT ) by A1e, A1d, XBOOLE_1:1, XBOOLE_1:28
.= (X0 /\ Y0) /\ NAT by XBOOLE_1:16
.= {} by A1, AG110 ;
then A72: X0 misses Y0 by XBOOLE_0:def 7;
A73: (X0 \/ Y0) \ X0 = (X0 \ X0) \/ (Y0 \ X0) by XBOOLE_1:42
.= {} \/ (Y0 \ X0) by XBOOLE_1:37
.= Y0 by A72, XBOOLE_1:83 ;
A4: len ((Sgm0 (X0 \/ Y0)) /^ (card X0)) = card Y0 by A74, A33, A73, CARD_2:63, XBOOLE_1:7;
len (Sgm0 (X0 \/ Y0)) = card (X0 \/ Y0) by Th44;
then A4e: len (Sgm0 (X0 \/ Y0)) = (card X0) + (card Y0) by A72, CARD_2:53;
B4: rng ((Sgm0 (X0 \/ Y0)) /^ (card X0)) c= rng (Sgm0 (X0 \/ Y0)) by AG170;
A3: rng ((Sgm0 (X0 \/ Y0)) /^ (card X0)) c= { v where v is Element of X0 \/ Y0 : ex k2 being Nat st
( v = ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . k2 & k2 in card Y0 ) }

proof

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

end;

A40n: { v where v is Element of X0 \/ Y0 : ex k2 being Nat st
( v = ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . k2 & k2 in card Y0 ) } c= rng ((Sgm0 (X0 \/ Y0)) /^ (card X0))

proof

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

end;

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

A50n: now

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

B36n: now

assume C0bn: x20 >= card X0 ; :: thesis: contradiction
then C0b: x20 -' (card X0) = x20 - (card X0) by XREAL_1:235;
x20 < (card X0) + (card Y0) by A4e, B5, NAT_1:45;
then x20 - (card X0) < ((card X0) + (card Y0)) - (card X0) by XREAL_1:11;
then C8: x20 -' (card X0) < card Y0 by C0bn, XREAL_1:235;
then C5e: (x20 -' (card X0)) + (card X0) < len (Sgm0 (X0 \/ Y0)) by A4e, XREAL_1:8;
C5: ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . (x20 -' (card X0)) = (Sgm0 (X0 \/ Y0)) . x20 by C0b, C5e, Th19b;
x20 -' (card X0) in card Y0 by C8, NAT_1:45;
hence contradiction by B3, C5, B5, B57d; :: thesis: verum

end;

card X0 <= (card X0) + k20 by NAT_1:12;
then B62: k20 + (card X0) > x20 by B36n, XXREAL_0:2;
k20 < card Y0 by B4b, NAT_1:45;
then B53: k20 + (card X0) < len (Sgm0 (X0 \/ Y0)) by A4e, XREAL_1:8;
then ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . k20 = (Sgm0 (X0 \/ Y0)) . (k20 + (card X0)) by Th19b;
then nv10 > nv2 by B5, B53, AC113, B62, B4b;
hence contradiction by AE100, A1, B3, B98; :: thesis: verum

end;

A51: dom ((Sgm0 (X0 \/ Y0)) /^ (card X0)),((Sgm0 (X0 \/ Y0)) /^ (card X0)) .: (dom ((Sgm0 (X0 \/ Y0)) /^ (card X0))) are_equipotent by CARD_1:60;
((Sgm0 (X0 \/ Y0)) /^ (card X0)) .: (dom ((Sgm0 (X0 \/ Y0)) /^ (card X0))) = rng ((Sgm0 (X0 \/ Y0)) /^ (card X0)) by RELAT_1:146;
then card { v where v is Element of X0 \/ Y0 : ex k2 being Nat st
( v = ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . k2 & k2 in card Y0 ) } = card (len ((Sgm0 (X0 \/ Y0)) /^ (card X0))) by A40, A51, CARD_1:21;
then A53: card { v where v is Element of X0 \/ Y0 : ex k2 being Nat st
( v = ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . k2 & k2 in card Y0 ) } = card Y0 by A74, A33, A73, CARD_2:63, XBOOLE_1:7;
then Y0,{ v where v is Element of X0 \/ Y0 : ex k2 being Nat st
( v = ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . k2 & k2 in card Y0 ) } are_equipotent by CARD_1:21;
then reconsider Z0 = { v where v is Element of X0 \/ Y0 : ex k2 being Nat st
( v = ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . k2 & k2 in card Y0 ) } as finite set by CARD_1:68;

A77n: now

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

case Z0 c= Y0 ; :: thesis: Z0 = Y0

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

end;

case Y0 c= Z0 ; :: thesis: Z0 = Y0

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

end;

end;

end;

i + (card X0) < len (Sgm0 (X0 \/ Y0)) by A1, A4, A74, XREAL_1:22;
hence ( rng ((Sgm0 (X0 \/ Y0)) /^ (card X0)) = Y0 & ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . i = (Sgm0 (X0 \/ Y0)) . (i + (card X0)) ) by A3, A40n, A77n, Th19b, XBOOLE_0:def 10; :: thesis: verum