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 2;
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:68;
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:68;
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:84;
reconsider j2 = j2 as Function of x1,x2 by A15, FUNCT_2:66;
reconsider j1 = j1 as Function of x2,x3 by A14, FUNCT_2:66;
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 2;
hence c . i is Function of ({|M,M|} . i),({|M|} . i) by A11, A16, A12, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum

end;

then reconsider c = c as BinComp of M by PBOOLE:def 15;
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 13 :: 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 2;
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:68 ; :: 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