deffunc H_{1}( 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_{1}(i,j,k)
from ALTCAT_1:sch 3();

c is Function-yielding

set C = AltCatStr(# A,M,c #);

AltCatStr(# A,M,c #) is pseudo-functional

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

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

c is Function-yielding

proof

then reconsider c = c as ManySortedFunction of [:A,A,A:] ;
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;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

now :: thesis: for i being object st i in [:A,A,A:] holds

c . i is Function of ({|M,M|} . i),({|M|} . i)

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

set C = AltCatStr(# A,M,c #);

AltCatStr(# A,M,c #) is pseudo-functional

proof

then reconsider C = AltCatStr(# A,M,c #) as non empty strict pseudo-functional AltCatStr ;
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;( <^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

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