let i be Nat; :: thesis: for X0, Y0 being finite natural-membered set st X0 <N< Y0 & i < card X0 holds
( rng ((Sgm0 (X0 \/ Y0)) | (card X0)) = X0 & ((Sgm0 (X0 \/ Y0)) | (card X0)) . i = (Sgm0 (X0 \/ Y0)) . i )
let X0, Y0 be finite natural-membered set ; :: thesis: ( X0 <N< Y0 & i < card X0 implies ( rng ((Sgm0 (X0 \/ Y0)) | (card X0)) = X0 & ((Sgm0 (X0 \/ Y0)) | (card X0)) . i = (Sgm0 (X0 \/ Y0)) . i ) )
assume that
A1: X0 <N< Y0 and
A2: i < card X0 ; :: thesis: ( rng ((Sgm0 (X0 \/ Y0)) | (card X0)) = X0 & ((Sgm0 (X0 \/ Y0)) | (card X0)) . i = (Sgm0 (X0 \/ Y0)) . i )
A3: i in Segm (card X0) by A2, NAT_1:44;
set f = (Sgm0 (X0 \/ Y0)) | (card X0);
set f0 = Sgm0 (X0 \/ Y0);
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 X0 ) } ;
A4: X0 c= X0 \/ Y0 by XBOOLE_1:7;
A5: len (Sgm0 (X0 \/ Y0)) = card (X0 \/ Y0) by Th20;
then A6: len ((Sgm0 (X0 \/ Y0)) | (card X0)) = card X0 by A4, AFINSQ_1:54, NAT_1:43;
A7: { v where v is Element of X0 \/ Y0 : ex k2 being Nat st
( v = ((Sgm0 (X0 \/ Y0)) | (card X0)) . k2 & k2 in card X0 ) } c= rng ((Sgm0 (X0 \/ Y0)) | (card X0))

proof

let y be object ; :: 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 X0 ) } 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 X0 ) } ; :: thesis: y in rng ((Sgm0 (X0 \/ Y0)) | (card X0))
then ex v0 being Element of X0 \/ Y0 st
( y = v0 & ex k2 being Nat st
( v0 = ((Sgm0 (X0 \/ Y0)) | (card X0)) . k2 & k2 in card X0 ) ) ;
hence y in rng ((Sgm0 (X0 \/ Y0)) | (card X0)) by A6, FUNCT_1:def 3; :: thesis: verum

end;

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 X0 ) } as finite set ;
(Sgm0 (X0 \/ Y0)) | (card X0) is one-to-one by FUNCT_1:52;
then A8: dom ((Sgm0 (X0 \/ Y0)) | (card X0)),((Sgm0 (X0 \/ Y0)) | (card X0)) .: (dom ((Sgm0 (X0 \/ Y0)) | (card X0))) are_equipotent by CARD_1:33;
A9: ((Sgm0 (X0 \/ Y0)) | (card X0)) .: (dom ((Sgm0 (X0 \/ Y0)) | (card X0))) = rng ((Sgm0 (X0 \/ Y0)) | (card X0)) by RELAT_1:113;
A10: len (Sgm0 (X0 \/ Y0)) = card (X0 \/ Y0) by Th20;
A11: rng (Sgm0 (X0 \/ Y0)) = X0 \/ Y0 by Def4;
A12: 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 X0 ) }

proof

let y be object ; :: 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 X0 ) } )
assume A13: 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 X0 ) }
then consider x being object such that
A14: x in dom ((Sgm0 (X0 \/ Y0)) | (card X0)) and
A15: y = ((Sgm0 (X0 \/ Y0)) | (card X0)) . x by FUNCT_1:def 3;
reconsider y0 = y as Element of X0 \/ Y0 by Def4, A13;
ex k2 being Nat st
( y0 = ((Sgm0 (X0 \/ Y0)) | (card X0)) . k2 & k2 in card X0 ) by A14, A15;
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 X0 ) } ; :: thesis: verum

end;

then 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 X0 ) } by A7;
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 X0 ) } = card (len ((Sgm0 (X0 \/ Y0)) | (card X0))) by A8, A9, CARD_1:5;
then A16: card { v where v is Element of X0 \/ Y0 : ex k2 being Nat st
( v = ((Sgm0 (X0 \/ Y0)) | (card X0)) . k2 & k2 in card X0 ) } = card X0 by A5, A4, AFINSQ_1:54, NAT_1:43;
A17: X0 \/ Y0 <> {} by A2, CARD_1:27, XBOOLE_1:15;

A18: now :: thesis: ( not { v where v is Element of X0 \/ Y0 : ex k2 being Nat st
( v = ((Sgm0 (X0 \/ Y0)) | (card X0)) . k2 & k2 in card X0 ) } c= X0 implies 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 X0 ) } )

assume that
A19: not { v where v is Element of X0 \/ Y0 : ex k2 being Nat st
( v = ((Sgm0 (X0 \/ Y0)) | (card X0)) . k2 & k2 in card X0 ) } c= X0 and
A20: not 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 X0 ) } ; :: thesis: contradiction
consider v1 being object such that
A21: 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 X0 ) } and
A22: not v1 in X0 by A19;
consider v10 being Element of X0 \/ Y0 such that
A23: v1 = v10 and
A24: ex k2 being Nat st
( v10 = ((Sgm0 (X0 \/ Y0)) | (card X0)) . k2 & k2 in card X0 ) by A21;
A25: v10 in Y0 by A17, A22, A23, XBOOLE_0:def 3;
reconsider nv10 = v10 as Nat ;
consider v2 being object such that
A26: v2 in X0 and
A27: 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 X0 ) } by A20;
X0 c= X0 \/ Y0 by XBOOLE_1:7;
then consider x2 being object such that
A28: x2 in dom (Sgm0 (X0 \/ Y0)) and
A29: v2 = (Sgm0 (X0 \/ Y0)) . x2 by A11, A26, FUNCT_1:def 3;
reconsider x20 = x2 as Nat by A28;
reconsider nv2 = v2 as Nat by A29;
A30: x20 < len (Sgm0 (X0 \/ Y0)) by A28, AFINSQ_1:86;

A31: now :: thesis: not x20 < card X0

assume x20 < card X0 ; :: thesis: contradiction
then A32: x20 in Segm (card X0) by NAT_1:44;
card X0 <= card (X0 \/ Y0) by NAT_1:43, XBOOLE_1:7;
then card X0 <= len (Sgm0 (X0 \/ Y0)) by Th20;
then ((Sgm0 (X0 \/ Y0)) | (card X0)) . x20 = (Sgm0 (X0 \/ Y0)) . x20 by A32, AFINSQ_1:53;
hence contradiction by A4, A26, A27, A29, A32; :: thesis: verum

end;

consider k20 being Nat such that
A33: v10 = ((Sgm0 (X0 \/ Y0)) | (card X0)) . k20 and
A34: k20 in card X0 by A24;
card X0 <= len (Sgm0 (X0 \/ Y0)) by A10, NAT_1:43, XBOOLE_1:7;
then A35: ((Sgm0 (X0 \/ Y0)) | (card X0)) . k20 = (Sgm0 (X0 \/ Y0)) . k20 by A34, AFINSQ_1:53;
k20 < len ((Sgm0 (X0 \/ Y0)) | (card X0)) by A6, A34, AFINSQ_1:86;
then k20 < x20 by A6, A31, XXREAL_0:2;
then nv10 < nv2 by A33, A29, A35, A30, Def4;
hence contradiction by A1, A26, A25; :: thesis: verum

end;

A36: now :: thesis: ( ( Z0 c= X0 & Z0 = X0 ) or ( X0 c= Z0 & Z0 = X0 ) )

per cases ( Z0 c= X0 or X0 c= Z0 ) by A18;

case Z0 c= X0 ; :: thesis: Z0 = X0

hence Z0 = X0 by A16, CARD_2:102; :: thesis: verum

end;

case X0 c= Z0 ; :: thesis: Z0 = X0

hence Z0 = X0 by A16, CARD_2:102; :: thesis: verum

end;

end;

end;

card X0 <= len (Sgm0 (X0 \/ Y0)) by A5, NAT_1:43, XBOOLE_1:7;
hence ( rng ((Sgm0 (X0 \/ Y0)) | (card X0)) = X0 & ((Sgm0 (X0 \/ Y0)) | (card X0)) . i = (Sgm0 (X0 \/ Y0)) . i ) by A12, A7, A36, A3, AFINSQ_1:53; :: thesis: verum