A1: {[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 [:1,1,1:] ;
reconsider c = c as ManySortedFunction of [:1,1,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 [:1,1:] by PARTFUN1:def 4, RELAT_1:def 18;
A2: m . 0 ,0 = Funcs 0 ,0 by FUNCOP_1:87;
A3: 0 in 1 by CARD_1:87, TARSKI:def 1;

now

let i be set ; :: thesis: ( i in [:1,1,1:] implies c . i is Function of ({|m,m|} . i),({|m|} . i) )
reconsider ci = c . i as Function ;
assume i in [:1,1,1:] ; :: thesis: c . i is Function of ({|m,m|} . i),({|m|} . i)
then A4: i = [0 ,0 ,0 ] by A1, TARSKI:def 1;
then A5: c . i = FuncComp (Funcs 0 ,0 ),(Funcs 0 ,0 ) by FUNCOP_1:87;
then A6: dom ci = [:(m . 0 ,0 ),(m . 0 ,0 ):] by A2, PARTFUN1:def 4
.= {|m,m|} . 0 ,0 ,0 by A3, Def6
.= {|m,m|} . i by A4, MULTOP_1:def 1 ;
A7: {|m|} . i = {|m|} . 0 ,0 ,0 by A4, MULTOP_1:def 1
.= m . 0 ,0 by A3, Def5 ;
then rng ci c= {|m|} . i by A2, A5, Th14;
hence c . i is Function of ({|m,m|} . i),({|m|} . i) by A2, A6, A7, 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^>:]
A8: o3 = 0 by CARD_1:87, TARSKI:def 1;
A9: ( o1 = 0 & o2 = 0 ) by CARD_1:87, TARSKI:def 1;
then A10: dom (FuncComp (Funcs 0 ,0 ),(Funcs 0 ,0 )) = [:<^o2,o3^>,<^o1,o2^>:] by A2, A8, 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, A8, FUNCOP_1:87
.= (FuncComp (Funcs o1,o2),(Funcs o2,o3)) | [:<^o2,o3^>,<^o1,o2^>:] by A9, A8, A10, RELAT_1:97 ; :: thesis: verum