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

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

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

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;

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

end;

end;

end;

c is Function-yielding

proof

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;

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

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