let i be Nat; for X0, Y0 being finite natural-membered set 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 X0, Y0 be finite natural-membered set ; ( 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 that
A1:
X0 <N< Y0
and
A2:
i < card Y0
; ( 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
A3:
Y0 c= Segm n
by Th2;
X0 /\ Y0 =
X0 /\ (Y0 /\ NAT)
by A3, XBOOLE_1:1, XBOOLE_1:28
.=
(X0 /\ Y0) /\ NAT
by XBOOLE_1:16
.=
{}
by A1, Th23
;
then A4:
X0 misses Y0
;
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 Y0 ) } ;
A5:
dom ((Sgm0 (X0 \/ Y0)) /^ (card X0)),((Sgm0 (X0 \/ Y0)) /^ (card X0)) .: (dom ((Sgm0 (X0 \/ Y0)) /^ (card X0))) are_equipotent
by CARD_1:33;
A6:
rng (Sgm0 (X0 \/ Y0)) = X0 \/ Y0
by Def4;
A7:
len (Sgm0 (X0 \/ Y0)) = card (X0 \/ Y0)
by Th20;
then A8:
card X0 <= len (Sgm0 (X0 \/ Y0))
by NAT_1:43, XBOOLE_1:7;
A9: len ((Sgm0 (X0 \/ Y0)) /^ (card X0)) =
(len (Sgm0 (X0 \/ Y0))) -' (card X0)
by Def2
.=
(len (Sgm0 (X0 \/ Y0))) - (card X0)
by A8, XREAL_1:233
;
A10: (X0 \/ Y0) \ X0 =
(X0 \ X0) \/ (Y0 \ X0)
by XBOOLE_1:42
.=
{} \/ (Y0 \ X0)
by XBOOLE_1:37
.=
Y0
by A4, XBOOLE_1:83
;
then A11:
len ((Sgm0 (X0 \/ Y0)) /^ (card X0)) = card Y0
by A7, A9, CARD_2:44, XBOOLE_1:7;
A12:
{ 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))
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 ;
A13:
((Sgm0 (X0 \/ Y0)) /^ (card X0)) .: (dom ((Sgm0 (X0 \/ Y0)) /^ (card X0))) = rng ((Sgm0 (X0 \/ Y0)) /^ (card X0))
by RELAT_1:113;
A14:
rng ((Sgm0 (X0 \/ Y0)) /^ (card X0)) c= rng (Sgm0 (X0 \/ Y0))
by Th9;
A15:
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 ) }
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 Y0 ) }
by A12;
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 A5, A13, CARD_1:5;
then A19:
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 A7, A9, A10, CARD_2:44, XBOOLE_1:7;
len (Sgm0 (X0 \/ Y0)) = card (X0 \/ Y0)
by Th20;
then A20:
len (Sgm0 (X0 \/ Y0)) = (card X0) + (card Y0)
by A4, CARD_2:40;
A21:
X0 \/ Y0 <> {}
by A2, CARD_1:27, XBOOLE_1:15;
A22:
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 Y0 ) } c= Y0 implies 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 ) } )assume that A23:
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
and A24:
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 ) }
;
contradictionconsider v2 being
object such that A25:
v2 in Y0
and A26:
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 A24;
Y0 c= X0 \/ Y0
by XBOOLE_1:7;
then consider x2 being
object such that A27:
x2 in dom (Sgm0 (X0 \/ Y0))
and A28:
v2 = (Sgm0 (X0 \/ Y0)) . x2
by A6, A25, FUNCT_1:def 3;
consider v1 being
object such that A29:
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 ) }
and A30:
not
v1 in Y0
by A23;
consider v10 being
Element of
X0 \/ Y0 such that A31:
v1 = v10
and A32:
ex
k2 being
Nat st
(
v10 = ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . k2 &
k2 in Segm (card Y0) )
by A29;
A33:
v10 in X0
by A21, A30, A31, XBOOLE_0:def 3;
reconsider nv10 =
v10 as
Nat ;
reconsider nv2 =
v2 as
Nat by A28;
consider k20 being
Nat such that A34:
v10 = ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . k20
and A35:
k20 in Segm (card Y0)
by A32;
A36:
k20 + (card X0) < len (Sgm0 (X0 \/ Y0))
by A20, XREAL_1:6, A35, NAT_1:44;
then A37:
((Sgm0 (X0 \/ Y0)) /^ (card X0)) . k20 = (Sgm0 (X0 \/ Y0)) . (k20 + (card X0))
by Th8;
reconsider x20 =
x2 as
Nat by A27;
set nx20 =
x20 -' (card X0);
A38:
v2 in X0 \/ Y0
by A6, A27, A28, FUNCT_1:def 3;
card X0 <= (card X0) + k20
by NAT_1:12;
then
k20 + (card X0) > x20
by A39, XXREAL_0:2;
then
nv10 > nv2
by A34, A28, A36, A37, Def4;
hence
contradiction
by A1, A25, A33;
verum end;
A44:
now ( ( Z0 c= Y0 & Z0 = Y0 ) or ( Y0 c= Z0 & Z0 = Y0 ) )end;
i + (card X0) < len (Sgm0 (X0 \/ Y0))
by A2, A9, A11, XREAL_1:20;
hence
( rng ((Sgm0 (X0 \/ Y0)) /^ (card X0)) = Y0 & ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . i = (Sgm0 (X0 \/ Y0)) . (i + (card X0)) )
by A15, A12, A44, Th8; verum