let i be Nat; 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 ; ( 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
; ( 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))
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 ) }
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 ( 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 ) }
;
contradictionconsider 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;
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;
verum end;
A36:
now ( ( Z0 c= X0 & Z0 = X0 ) or ( X0 c= Z0 & Z0 = X0 ) )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; verum