set X = {0 ,1};
set Y = Necklace 4;
reconsider r = id {0 ,1} as Relation of {0 ,1} by RELSET_1:29;
take R = RelStr(# {0 ,1},r #); :: thesis: ( R is strict & R is finite & R is N-free )
now let f be
Function of
(Necklace 4),
R;
:: thesis: ( 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) ) ) )assume A1:
f is
one-to-one
;
:: thesis: 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 )A2:
dom f =
the
carrier of
(Necklace 4)
by FUNCT_2:def 1
.=
{0 ,1,2,3}
by NECKLACE:2, NECKLACE:21
;
then A3:
1
in dom f
by ENUMSET1:def 2;
A4:
2
in dom f
by A2, ENUMSET1:def 2;
A5:
3
in dom f
by A2, ENUMSET1:def 2;
then A6:
f . 1
<> f . 3
by A1, A3, FUNCT_1:def 8;
A7:
f . 2
<> f . 3
by A1, A4, A5, FUNCT_1:def 8;
A8:
f . 1
in {0 ,1}
by A3, PARTFUN1:27;
A9:
f . 2
in {0 ,1}
by A4, PARTFUN1:27;
A10:
f . 3
in {0 ,1}
by A5, PARTFUN1:27;
A11:
(
f . 1
= 0 or
f . 1
= 1 )
by A8, TARSKI:def 2;
(
f . 2
= 0 or
f . 2
= 1 )
by A9, TARSKI:def 2;
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 A1, A3, A4, A6, A7, A10, A11, FUNCT_1:def 8, TARSKI:def 2;
:: thesis: verum end;
then
not R embeds Necklace 4
by NECKLACE:def 2;
hence
( R is strict & R is finite & R is N-free )
by Def1; :: thesis: verum