deffunc H1( Element of A, set , set ) -> set = IFEQ ($1,$2,(IFEQ ($2,$3,([(id $1),(id $1)] .--> (id $1)),{})),{});
deffunc H2( Element of A, set ) -> set = IFEQ ($1,$2,{(id $1)},{});
consider M being ManySortedSet of [:A,A:] such that
A1:
for i, j being Element of A holds M . (i,j) = H2(i,j)
from ALTCAT_1:sch 2();
consider c being ManySortedSet of [:A,A,A:] such that
A2:
for i, j, k being Element of A holds c . (i,j,k) = H1(i,j,k)
from ALTCAT_1:sch 4();
A3:
now for i being object st i in [:A,A,A:] holds
c . i is Function of ({|M,M|} . i),({|M|} . i)let i be
object ;
( i in [:A,A,A:] implies c . b1 is Function of ({|M,M|} . b1),({|M|} . b1) )assume
i in [:A,A,A:]
;
c . b1 is Function of ({|M,M|} . b1),({|M|} . b1)then consider i1,
i2,
i3 being
object such that A4:
(
i1 in A &
i2 in A &
i3 in A )
and A5:
i = [i1,i2,i3]
by MCART_1:68;
reconsider i1 =
i1,
i2 =
i2,
i3 =
i3 as
Element of
A by A4;
per cases
( ( i1 = i2 & i2 = i3 ) or i1 <> i2 or i2 <> i3 )
;
suppose that A6:
i1 = i2
and A7:
i2 = i3
;
c . b1 is Function of ({|M,M|} . b1),({|M|} . b1)A8:
M . (
i1,
i1) =
IFEQ (
i1,
i1,
{(id i1)},
{})
by A1
.=
{(id i1)}
by FUNCOP_1:def 8
;
A9:
c . i =
c . (
i1,
i2,
i3)
by A5, MULTOP_1:def 1
.=
IFEQ (
i1,
i2,
(IFEQ (i2,i3,([(id i1),(id i1)] .--> (id i1)),{})),
{})
by A2
.=
IFEQ (
i2,
i3,
([(id i1),(id i1)] .--> (id i1)),
{})
by A6, FUNCOP_1:def 8
.=
[(id i1),(id i1)] .--> (id i1)
by A7, FUNCOP_1:def 8
;
A10:
{|M|} . i =
{|M|} . (
i1,
i1,
i1)
by A5, A6, A7, MULTOP_1:def 1
.=
{(id i1)}
by A8, Def3
;
A11:
{|M,M|} . i =
{|M,M|} . (
i1,
i1,
i1)
by A5, A6, A7, MULTOP_1:def 1
.=
[:{(id i1)},{(id i1)}:]
by A8, Def4
.=
{[(id i1),(id i1)]}
by ZFMISC_1:29
.=
dom ([(id i1),(id i1)] .--> (id i1))
;
thus
c . i is
Function of
({|M,M|} . i),
({|M|} . i)
by A9, A10, A11;
verum end; suppose A12:
(
i1 <> i2 or
i2 <> i3 )
;
c . b1 is Function of ({|M,M|} . b1),({|M|} . b1)A13:
now c . i = {} per cases
( i1 <> i2 or ( i1 = i2 & i2 <> i3 ) )
by A12;
suppose A14:
i1 <> i2
;
c . i = {} thus c . i =
c . (
i1,
i2,
i3)
by A5, MULTOP_1:def 1
.=
IFEQ (
i1,
i2,
(IFEQ (i2,i3,([(id i1),(id i1)] .--> (id i1)),{})),
{})
by A2
.=
{}
by A14, FUNCOP_1:def 8
;
verum end; suppose that A15:
i1 = i2
and A16:
i2 <> i3
;
c . i = {} thus c . i =
c . (
i1,
i2,
i3)
by A5, MULTOP_1:def 1
.=
IFEQ (
i1,
i2,
(IFEQ (i2,i3,([(id i1),(id i1)] .--> (id i1)),{})),
{})
by A2
.=
IFEQ (
i2,
i3,
([(id i1),(id i1)] .--> (id i1)),
{})
by A15, FUNCOP_1:def 8
.=
{}
by A16, FUNCOP_1:def 8
;
verum end; end; end;
(
M . (
i1,
i2)
= IFEQ (
i1,
i2,
{(id i1)},
{}) &
M . (
i2,
i3)
= IFEQ (
i2,
i3,
{(id i2)},
{}) )
by A1;
then A17:
(
M . (
i1,
i2)
= {} or
M . (
i2,
i3)
= {} )
by A12, FUNCOP_1:def 8;
{|M,M|} . i =
{|M,M|} . (
i1,
i2,
i3)
by A5, MULTOP_1:def 1
.=
[:(M . (i2,i3)),(M . (i1,i2)):]
by Def4
.=
{}
by A17
;
hence
c . i is
Function of
({|M,M|} . i),
({|M|} . i)
by A13, FUNCT_2:2, RELAT_1:38, XBOOLE_1:2;
verum end; end; end;
c is Function-yielding
then reconsider c = c as ManySortedFunction of [:A,A,A:] ;
reconsider c = c as BinComp of M by A3, PBOOLE:def 15;
set C = AltCatStr(# A,M,c #);
AltCatStr(# A,M,c #) is quasi-discrete
proof
let o1,
o2 be
Object of
AltCatStr(#
A,
M,
c #);
ALTCAT_1:def 18 ( <^o1,o2^> <> {} implies o1 = o2 )
assume that A18:
<^o1,o2^> <> {}
and A19:
o1 <> o2
;
contradiction
<^o1,o2^> =
IFEQ (
o1,
o2,
{(id o1)},
{})
by A1
.=
{}
by A19, FUNCOP_1:def 8
;
hence
contradiction
by A18;
verum
end;
then reconsider C = AltCatStr(# A,M,c #) as non empty strict quasi-discrete AltCatStr ;
take
C
; ( the carrier of C = A & ( for i being Object of C holds <^i,i^> = {(id i)} ) )
thus
the carrier of C = A
; for i being Object of C holds <^i,i^> = {(id i)}
let i be Object of C; <^i,i^> = {(id i)}
thus <^i,i^> =
IFEQ (i,i,{(id i)},{})
by A1
.=
{(id i)}
by FUNCOP_1:def 8
; verum