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 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 Th31;
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 ;
A8:
rng ((Sgm0 (X0 \/ Y0)) | (card X0)) c= rng (Sgm0 (X0 \/ Y0))
by RELAT_1:70;
(Sgm0 (X0 \/ Y0)) | (card X0) is one-to-one
by FUNCT_1:52;
then A9:
dom ((Sgm0 (X0 \/ Y0)) | (card X0)),((Sgm0 (X0 \/ Y0)) | (card X0)) .: (dom ((Sgm0 (X0 \/ Y0)) | (card X0))) are_equipotent
by CARD_1:33;
A10:
((Sgm0 (X0 \/ Y0)) | (card X0)) .: (dom ((Sgm0 (X0 \/ Y0)) | (card X0))) = rng ((Sgm0 (X0 \/ Y0)) | (card X0))
by RELAT_1:113;
A11:
len (Sgm0 (X0 \/ Y0)) = card (X0 \/ Y0)
by Th31;
A12:
rng (Sgm0 (X0 \/ Y0)) = X0 \/ Y0
by Def5;
A13:
dom ((Sgm0 (X0 \/ Y0)) | (card X0)) = len ((Sgm0 (X0 \/ Y0)) | (card X0))
;
A14:
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, XBOOLE_0:def 10;
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 A9, A10, CARD_1:5;
then A18:
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;
A19:
X0 \/ Y0 <> {}
by A2, CARD_1:27, XBOOLE_1:15;
A20:
now assume that A21:
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 A22:
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
set such that A23:
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 A24:
not
v1 in X0
by A21, TARSKI:def 3;
consider v10 being
Element of
X0 \/ Y0 such that A25:
v1 = v10
and A26:
ex
k2 being
Nat st
(
v10 = ((Sgm0 (X0 \/ Y0)) | (card X0)) . k2 &
k2 in card X0 )
by A23;
A27:
v10 in Y0
by A19, A24, A25, XBOOLE_0:def 3;
reconsider nv10 =
v10 as
Nat ;
consider v2 being
set such that A28:
v2 in X0
and A29:
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 A22, TARSKI:def 3;
X0 c= X0 \/ Y0
by XBOOLE_1:7;
then consider x2 being
set such that A30:
x2 in dom (Sgm0 (X0 \/ Y0))
and A31:
v2 = (Sgm0 (X0 \/ Y0)) . x2
by A12, A28, FUNCT_1:def 3;
reconsider x20 =
x2 as
Nat by A30;
reconsider nv2 =
v2 as
Nat by A31;
A32:
x20 < len (Sgm0 (X0 \/ Y0))
by A30, NAT_1:44;
consider k20 being
Nat such that A35:
v10 = ((Sgm0 (X0 \/ Y0)) | (card X0)) . k20
and A36:
k20 in card X0
by A26;
card X0 <= len (Sgm0 (X0 \/ Y0))
by A11, NAT_1:43, XBOOLE_1:7;
then A37:
((Sgm0 (X0 \/ Y0)) | (card X0)) . k20 = (Sgm0 (X0 \/ Y0)) . k20
by A36, AFINSQ_1:53;
k20 < len ((Sgm0 (X0 \/ Y0)) | (card X0))
by A6, A36, NAT_1:44;
then
k20 < x20
by A6, A33, XXREAL_0:2;
then
nv10 < nv2
by A35, A31, A37, A32, Def5;
hence
contradiction
by A1, A28, A27, Def6;
verum 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 A14, A7, A38, A3, AFINSQ_1:53, XBOOLE_0:def 10; verum