deffunc H₁( Element of A, set , set ) -> set = IFEQ $1,$2,(IFEQ $2,$3,([(id $1),(id $1)] .--> (id $1)),{} ),{} ;
deffunc H₂( 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₂(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₁(i,j,k) from ALTCAT_1:sch 4();

A3: now

let i be set ; :: thesis: ( i in [:A,A,A:] implies c . b₁ is Function of ({|M,M|} . b₁),({|M|} . b₁) )
assume i in [:A,A,A:] ; :: thesis: c . b₁ is Function of ({|M,M|} . b₁),({|M|} . b₁)
then consider i1, i2, i3 being set such that
A4: ( i1 in A & i2 in A & i3 in A ) and
A5: i = [i1,i2,i3] by MCART_1:72;
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 ; :: thesis: c . b₁ is Function of ({|M,M|} . b₁),({|M|} . 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, Def5 ;
{|M,M|} . i = {|M,M|} . i1,i1,i1 by A5, A6, A7, MULTOP_1:def 1
.= [:{(id i1)},{(id i1)}:] by A8, Def6
.= {[(id i1),(id i1)]} by ZFMISC_1:35
.= dom ([(id i1),(id i1)] .--> (id i1)) by FUNCOP_1:19 ;
hence c . i is Function of ({|M,M|} . i),({|M|} . i) by A9, A10, FUNCT_2:def 1; :: thesis: verum

end;

suppose A11: ( i1 <> i2 or i2 <> i3 ) ; :: thesis: c . b₁ is Function of ({|M,M|} . b₁),({|M|} . b₁)

A12: now

per cases ( i1 <> i2 or ( i1 = i2 & i2 <> i3 ) ) by A11;

suppose A13: 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 A13, FUNCOP_1:def 8 ; :: thesis: verum

end;

suppose that A14: i1 = i2 and
A15: 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 A14, FUNCOP_1:def 8
.= {} by A15, FUNCOP_1:def 8 ; :: thesis: verum

end;

end;

end;

( M . i1,i2 = IFEQ i1,i2,{(id i1)},{} & M . i2,i3 = IFEQ i2,i3,{(id i2)},{} ) by A1;
then A16: ( M . i1,i2 = {} or M . i2,i3 = {} ) by A11, 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 Def6
.= {} by A16 ;
hence c . i is Function of ({|M,M|} . i),({|M|} . i) by A12, FUNCT_2:def 1, RELAT_1:60, XBOOLE_1:2; :: thesis: verum

end;

end;

end;

c is Function-yielding

proof

let i be set ; :: 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:] by PARTFUN1:def 4;
hence c . i is set by A3; :: thesis: verum

end;

then reconsider c = c as ManySortedFunction of [:A,A,A:] ;
reconsider c = c as BinComp of M by A3, PBOOLE:def 18;
set C = AltCatStr(# A,M,c #);
AltCatStr(# A,M,c #) is quasi-discrete

proof

let o1, o2 be object of AltCatStr(# A,M,c #); :: according to ALTCAT_1:def 20 :: thesis: ( <^o1,o2^> <> {} implies o1 = o2 )
assume that
A17: <^o1,o2^> <> {} and
A18: o1 <> o2 ; :: thesis: contradiction
<^o1,o2^> = IFEQ o1,o2,{(id o1)},{} by A1
.= {} by A18, FUNCOP_1:def 8 ;
hence contradiction by A17; :: thesis: verum

end;

then reconsider C = AltCatStr(# A,M,c #) as non empty strict quasi-discrete AltCatStr ;
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