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();
deffunc H₂( Element of A, set , set ) -> set = IFEQ $1,$2,(IFEQ $2,$3,([(id $1),(id $1)] .--> (id $1)),{} ),{} ;
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: 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 ;
A9: M . i1,i1 = IFEQ i1,i1,{(id i1)},{} by A1
.= {(id i1)} by FUNCOP_1:def 8 ;
A10: {|M,M|} . i = {|M,M|} . i1,i1,i1 by A5, A6, A7, MULTOP_1:def 1
.= [:{(id i1)},{(id i1)}:] by A9, Def6
.= {[(id i1),(id i1)]} by ZFMISC_1:35
.= dom ([(id i1),(id i1)] .--> (id i1)) by FUNCOP_1:19 ;
A11: {|M|} . i = {|M|} . i1,i1,i1 by A5, A6, A7, MULTOP_1:def 1
.= {(id i1)} by A9, Def5 ;
thus c . i is Function of {|M,M|} . i,{|M|} . i by A8, A10, A11, FUNCT_2:def 1; :: thesis: verum

end;

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

A13: now

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

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;

suppose that A15: i1 = i2 and
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;

end;

end;

A17: M . i1,i2 = IFEQ i1,i2,{(id i1)},{} by A1;
M . i2,i3 = IFEQ i2,i3,{(id i2)},{} by A1;
then A18: ( M . i1,i2 = {} or M . i2,i3 = {} ) by A12, A17, FUNCOP_1:def 8;
A19: {|M,M|} . i = {|M,M|} . i1,i2,i3 by A5, MULTOP_1:def 1
.= [:(M . i2,i3),(M . i1,i2):] by Def6
.= {} by A18, ZFMISC_1:113 ;
{} c= {|M|} . i by XBOOLE_1:2;
hence c . i is Function of {|M,M|} . i,{|M|} . i by A13, A19, FUNCT_2:def 1, RELAT_1:60, RELSET_1:11; :: thesis: verum

end;

end;

end;

c is Function-yielding

proof

let i be set ; :: according to FUNCOP_1:def 6 :: thesis: ( not i in dom c or c . i is set )
assume i in dom c ; :: thesis: c . i is set
then i in [:A,A,A:] by PBOOLE:def 3;
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
A20: <^o1,o2^> <> {} and
A21: o1 <> o2 ; :: thesis: contradiction
<^o1,o2^> = IFEQ o1,o2,{(id o1)},{} by A1
.= {} by A21, FUNCOP_1:def 8 ;
hence contradiction by A20; :: 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