A1: 0 in 1 by CARD_1:87, TARSKI:def 1;
dom ([0 ,0 ] .--> (Funcs 0 ,0 )) = {[0 ,0 ]} by FUNCOP_1:19
.= [:1,1:] by CARD_1:87, ZFMISC_1:35 ;
then reconsider m = [0 ,0 ] .--> (Funcs 0 ,0 ) as ManySortedSet of by PARTFUN1:def 4, RELAT_1:def 18;
A3: {[0 ,0 ,0 ]} = [:1,1,1:] by CARD_1:87, MCART_1:39;
then reconsider c = [0 ,0 ,0 ] .--> (FuncComp (Funcs 0 ,0 ),(Funcs 0 ,0 )) as ManySortedSet of ;
reconsider c = c as ManySortedFunction of ;
A4: m . 0 ,0 = Funcs 0 ,0 by FUNCOP_1:87;

now

let i be set ; :: thesis: ( i in [:1,1,1:] implies c . i is Function of ({|m,m|} . i),({|m|} . i) )
assume i in [:1,1,1:] ; :: thesis: c . i is Function of ({|m,m|} . i),({|m|} . i)
then A5: i = [0 ,0 ,0 ] by A3, TARSKI:def 1;
then A6: c . i = FuncComp (Funcs 0 ,0 ),(Funcs 0 ,0 ) by FUNCOP_1:87;
reconsider ci = c . i as Function ;
A7: dom ci = [:(m . 0 ,0 ),(m . 0 ,0 ):] by A4, A6, PARTFUN1:def 4
.= {|m,m|} . 0 ,0 ,0 by A1, Def6
.= {|m,m|} . i by A5, MULTOP_1:def 1 ;
A8: {|m|} . i = {|m|} . 0 ,0 ,0 by A5, MULTOP_1:def 1
.= m . 0 ,0 by A1, Def5 ;
then rng ci c= {|m|} . i by A4, A6, Th14;
hence c . i is Function of ({|m,m|} . i),({|m|} . i) by A4, A7, A8, FUNCT_2:def 1, RELSET_1:11; :: thesis: verum

end;

then reconsider c = c as BinComp of m by PBOOLE:def 18;
take C = AltCatStr(# 1,m,c #); :: thesis: ( C is strict & C is pseudo-functional )
thus C is strict ; :: thesis: C is pseudo-functional
let o1, o2, o3 be object of C; :: according to ALTCAT_1:def 15 :: thesis: the Comp of C . o1,o2,o3 = (FuncComp (Funcs o1,o2),(Funcs o2,o3)) | [:<^o2,o3^>,<^o1,o2^>:]
A9: ( o1 = 0 & o2 = 0 & o3 = 0 ) by CARD_1:87, TARSKI:def 1;
then A10: dom (FuncComp (Funcs 0 ,0 ),(Funcs 0 ,0 )) = [:<^o2,o3^>,<^o1,o2^>:] by A4, PARTFUN1:def 4;
thus the Comp of C . o1,o2,o3 = c . [o1,o2,o3] by MULTOP_1:def 1
.= FuncComp (Funcs 0 ,0 ),(Funcs 0 ,0 ) by A9, FUNCOP_1:87
.= (FuncComp (Funcs o1,o2),(Funcs o2,o3)) | [:<^o2,o3^>,<^o1,o2^>:] by A9, A10, RELAT_1:97 ; :: thesis: verum