deffunc H_{1}( Element of A, set , set ) -> set = IFEQ ($1,$2,(IFEQ ($2,$3,([(id $1),(id $1)] .--> (id $1)),{})),{});

deffunc H_{2}( 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) = H_{2}(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) = H_{1}(i,j,k)
from ALTCAT_1:sch 4();

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

take C ; :: thesis: ( the carrier of C = A & ( for i being Object of C holds <^i,i^> = {(id i)} ) )

thus the carrier of C = A ; :: thesis: for i being Object of C holds <^i,i^> = {(id i)}

let i be Object of C; :: thesis: <^i,i^> = {(id i)}

thus <^i,i^> = IFEQ (i,i,{(id i)},{}) by A1

.= {(id i)} by FUNCOP_1:def 8 ; :: thesis: verum

deffunc H

consider M being ManySortedSet of [:A,A:] such that

A1: for i, j being Element of A holds M . (i,j) = H

consider c being ManySortedSet of [:A,A,A:] such that

A2: for i, j, k being Element of A holds c . (i,j,k) = H

A3: now :: thesis: for i being object st i in [:A,A,A:] holds

c . i is Function of ({|M,M|} . i),({|M|} . i)

c is Function-yielding
c . i is Function of ({|M,M|} . i),({|M|} . i)

let i be object ; :: thesis: ( i in [:A,A,A:] implies c . b_{1} is Function of ({|M,M|} . b_{1}),({|M|} . b_{1}) )

assume i in [:A,A,A:] ; :: thesis: c . b_{1} is Function of ({|M,M|} . b_{1}),({|M|} . b_{1})

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;

end;assume i in [:A,A,A:] ; :: thesis: c . b

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 )
;

end;

suppose that A6:
i1 = i2
and

A7: i2 = i3 ; :: thesis: c . b_{1} is Function of ({|M,M|} . b_{1}),({|M|} . b_{1})

A7: i2 = i3 ; :: thesis: c . b

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; :: thesis: verum

end;.= {(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; :: thesis: verum

suppose A12:
( i1 <> i2 or i2 <> i3 )
; :: thesis: c . b_{1} is Function of ({|M,M|} . b_{1}),({|M|} . b_{1})

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; :: thesis: verum

end;

A13: now :: thesis: c . i = {} end;

( M . (i1,i2) = IFEQ (i1,i2,{(id i1)},{}) & M . (i2,i3) = IFEQ (i2,i3,{(id i2)},{}) )
by A1;per cases
( i1 <> i2 or ( i1 = i2 & i2 <> i3 ) )
by A12;

end;

suppose A14:
i1 <> i2
; :: thesis: 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 ; :: thesis: verum

end;.= IFEQ (i1,i2,(IFEQ (i2,i3,([(id i1),(id i1)] .--> (id i1)),{})),{}) by A2

.= {} by A14, FUNCOP_1:def 8 ; :: thesis: verum

suppose that A15:
i1 = i2
and

A16: i2 <> i3 ; :: thesis: c . i = {}

A16: i2 <> i3 ; :: thesis: 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 ; :: thesis: verum

end;.= 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 ; :: thesis: verum

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; :: thesis: verum

proof

then reconsider c = c as ManySortedFunction of [:A,A,A:] ;
let i be object ; :: according to FUNCOP_1:def 6 :: thesis: ( not i in proj1 c or c . i is set )

assume i in dom c ; :: thesis: c . i is set

then i in [:A,A,A:] ;

hence c . i is set by A3; :: thesis: verum

end;assume i in dom c ; :: thesis: c . i is set

then i in [:A,A,A:] ;

hence c . i is set by A3; :: thesis: verum

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

then reconsider C = AltCatStr(# A,M,c #) as non empty strict quasi-discrete AltCatStr ;
let o1, o2 be Object of AltCatStr(# A,M,c #); :: according to ALTCAT_1:def 18 :: thesis: ( <^o1,o2^> <> {} implies o1 = o2 )

assume that

A18: <^o1,o2^> <> {} and

A19: o1 <> o2 ; :: thesis: contradiction

<^o1,o2^> = IFEQ (o1,o2,{(id o1)},{}) by A1

.= {} by A19, FUNCOP_1:def 8 ;

hence contradiction by A18; :: thesis: verum

end;assume that

A18: <^o1,o2^> <> {} and

A19: o1 <> o2 ; :: thesis: contradiction

<^o1,o2^> = IFEQ (o1,o2,{(id o1)},{}) by A1

.= {} by A19, FUNCOP_1:def 8 ;

hence contradiction by A18; :: thesis: verum

take C ; :: thesis: ( the carrier of C = A & ( for i being Object of C holds <^i,i^> = {(id i)} ) )

thus the carrier of C = A ; :: thesis: for i being Object of C holds <^i,i^> = {(id i)}

let i be Object of C; :: thesis: <^i,i^> = {(id i)}

thus <^i,i^> = IFEQ (i,i,{(id i)},{}) by A1

.= {(id i)} by FUNCOP_1:def 8 ; :: thesis: verum