set X = {0,1};
set Y = Necklace 4;
reconsider r = id {0,1} as Relation of {0,1} by RELSET_1:14;
take R = RelStr(# {0,1},r #); ( R is strict & R is finite & R is N-free )
now for f being Function of (Necklace 4),R st f is one-to-one holds
ex x, y being Element of (Necklace 4) st
( ( [x,y] in the InternalRel of (Necklace 4) implies [(f . x),(f . y)] in the InternalRel of R ) implies ( [(f . x),(f . y)] in the InternalRel of R & not [x,y] in the InternalRel of (Necklace 4) ) )let f be
Function of
(Necklace 4),
R;
( f is one-to-one implies ex x, y being Element of (Necklace 4) st
( ( [x,y] in the InternalRel of (Necklace 4) implies [(f . x),(f . y)] in the InternalRel of R ) implies ( [(f . x),(f . y)] in the InternalRel of R & not [x,y] in the InternalRel of (Necklace 4) ) ) )A1:
dom f =
the
carrier of
(Necklace 4)
by FUNCT_2:def 1
.=
{0,1,2,3}
by NECKLACE:1, NECKLACE:20
;
then A2:
3
in dom f
by ENUMSET1:def 2;
then A3:
f . 3
in {0,1}
by PARTFUN1:4;
A4:
2
in dom f
by A1, ENUMSET1:def 2;
then
f . 2
in {0,1}
by PARTFUN1:4;
then A5:
(
f . 2
= 0 or
f . 2
= 1 )
by TARSKI:def 2;
A6:
1
in dom f
by A1, ENUMSET1:def 2;
then
f . 1
in {0,1}
by PARTFUN1:4;
then A7:
(
f . 1
= 0 or
f . 1
= 1 )
by TARSKI:def 2;
assume A8:
f is
one-to-one
;
not for x, y being Element of (Necklace 4) holds
( [x,y] in the InternalRel of (Necklace 4) iff [(f . x),(f . y)] in the InternalRel of R )then A9:
f . 2
<> f . 3
by A4, A2, FUNCT_1:def 4;
f . 1
<> f . 3
by A8, A6, A2, FUNCT_1:def 4;
hence
not for
x,
y being
Element of
(Necklace 4) holds
(
[x,y] in the
InternalRel of
(Necklace 4) iff
[(f . x),(f . y)] in the
InternalRel of
R )
by A8, A6, A4, A9, A3, A7, A5, FUNCT_1:def 4, TARSKI:def 2;
verum end;
then
not R embeds Necklace 4
by NECKLACE:def 1;
hence
( R is strict & R is finite & R is N-free )
; verum