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 :: 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 . b1 is Function of ({|M,M|} . b1),({|M|} . b1) )
assume i in [:A,A,A:] ; :: thesis: 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 ; :: thesis: 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; :: thesis: verum
end;
suppose A12: ( i1 <> i2 or i2 <> i3 ) ; :: thesis: c . b1 is Function of ({|M,M|} . b1),({|M|} . b1)
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