deffunc H₁( set , set , set ) -> compositional ManySortedFunction of [:(Funcs $2,$3),(Funcs $1,$2):] = FuncComp (Funcs $1,$2),(Funcs $2,$3);
consider M being ManySortedSet of [:A,A:] such that
A1: for i, j being set st i in A & j in A holds
M . i,j = Funcs i,j from ALTCAT_1:sch 1();
consider c being ManySortedSet of [:A,A,A:] such that
A2: for i, j, k being set st i in A & j in A & k in A holds
c . i,j,k = H₁(i,j,k) from ALTCAT_1:sch 3();
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;
then consider x1, x2, x3 being set such that
A3: ( x1 in A & x2 in A & x3 in A ) and
A4: i = [x1,x2,x3] by MCART_1:72;
c . i = c . x1,x2,x3 by A4, MULTOP_1:def 1
.= FuncComp (Funcs x1,x2),(Funcs x2,x3) by A2, A3 ;
hence c . i is set ; :: thesis: verum

end;

then reconsider c = c as ManySortedFunction of [:A,A,A:] ;

now

let i be set ; :: thesis: ( i in [:A,A,A:] implies c . i is Function of ({|M,M|} . i),({|M|} . i) )
reconsider ci = c . i as Function ;
assume i in [:A,A,A:] ; :: thesis: c . i is Function of ({|M,M|} . i),({|M|} . i)
then consider x1, x2, x3 being set such that
A5: x1 in A and
A6: x2 in A and
A7: x3 in A and
A8: i = [x1,x2,x3] by MCART_1:72;
A9: {|M|} . i = {|M|} . x1,x2,x3 by A8, MULTOP_1:def 1
.= M . x1,x3 by A5, A6, A7, Def5 ;
A10: c . i = c . x1,x2,x3 by A8, MULTOP_1:def 1
.= FuncComp (Funcs x1,x2),(Funcs x2,x3) by A2, A5, A6, A7 ;
( M . x1,x2 = Funcs x1,x2 & M . x2,x3 = Funcs x2,x3 ) by A1, A5, A6, A7;
then A11: [:(Funcs x2,x3),(Funcs x1,x2):] = {|M,M|} . x1,x2,x3 by A5, A6, A7, Def6
.= {|M,M|} . i by A8, MULTOP_1:def 1 ;

A12: now

assume {|M,M|} . i <> {} ; :: thesis: {|M|} . i <> {}
then consider j being set such that
A13: j in [:(Funcs x2,x3),(Funcs x1,x2):] by A11, XBOOLE_0:def 1;
consider j1, j2 being set such that
A14: j1 in Funcs x2,x3 and
A15: j2 in Funcs x1,x2 and
j = [j1,j2] by A13, ZFMISC_1:103;
reconsider j2 = j2 as Function of x1,x2 by A15, FUNCT_2:121;
reconsider j1 = j1 as Function of x2,x3 by A14, FUNCT_2:121;
j1 * j2 in Funcs x1,x3 by A14, A15, Th4;
hence {|M|} . i <> {} by A1, A5, A7, A9; :: thesis: verum

end;

M . x1,x3 = Funcs x1,x3 by A1, A5, A7;
then A16: rng ci c= {|M|} . i by A10, A9, Th14;
dom ci = [:(Funcs x2,x3),(Funcs x1,x2):] by A10, PARTFUN1:def 4;
hence c . i is Function of ({|M,M|} . i),({|M|} . i) by A11, A16, A12, FUNCT_2:def 1, RELSET_1:11; :: thesis: verum

end;

then reconsider c = c as BinComp of M by PBOOLE:def 18;
set C = AltCatStr(# A,M,c #);
AltCatStr(# A,M,c #) is pseudo-functional

proof

let o1, o2, o3 be object of AltCatStr(# A,M,c #); :: according to ALTCAT_1:def 15 :: thesis: the Comp of AltCatStr(# A,M,c #) . o1,o2,o3 = (FuncComp (Funcs o1,o2),(Funcs o2,o3)) | [:<^o2,o3^>,<^o1,o2^>:]
( <^o1,o2^> = Funcs o1,o2 & <^o2,o3^> = Funcs o2,o3 ) by A1;
then A17: dom (FuncComp (Funcs o1,o2),(Funcs o2,o3)) = [:<^o2,o3^>,<^o1,o2^>:] by PARTFUN1:def 4;
thus the Comp of AltCatStr(# A,M,c #) . o1,o2,o3 = FuncComp (Funcs o1,o2),(Funcs o2,o3) by A2
.= (FuncComp (Funcs o1,o2),(Funcs o2,o3)) | [:<^o2,o3^>,<^o1,o2^>:] by A17, RELAT_1:97 ; :: thesis: verum

end;

then reconsider C = AltCatStr(# A,M,c #) as non empty strict pseudo-functional AltCatStr ;
take C ; :: thesis: ( the carrier of C = A & ( for a1, a2 being object of C holds <^a1,a2^> = Funcs a1,a2 ) )
thus the carrier of C = A ; :: thesis: for a1, a2 being object of C holds <^a1,a2^> = Funcs a1,a2
let a1, a2 be object of C; :: thesis: <^a1,a2^> = Funcs a1,a2
thus <^a1,a2^> = Funcs a1,a2 by A1; :: thesis: verum