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 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:] ;
then consider x1, x2, x3 being object such that
A3: ( x1 in A & x2 in A & x3 in A ) and
A4: i = [x1,x2,x3] by MCART_1:68;
reconsider x1 = x1, x2 = x2, x3 = x3 as set by TARSKI:1;
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 :: 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 . 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 object 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, Def3 ;
reconsider x1 = x1, x2 = x2, x3 = x3 as set by TARSKI:1;
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, Def4
.= {|M,M|} . i by A8, MULTOP_1:def 1 ;
M . (x1,x3) = Funcs (x1,x3) by A1, A5, A7;
then A12: rng ci c= {|M|} . i by A10, A9, Th6;
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, A12, FUNCT_2:2; :: 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 A13: 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 A13 ; :: 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