A1: {[0,0,0]} = [:1,1,1:] by CARD_1:49, MCART_1:35;
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:13
.= [:1,1:] by CARD_1:49, ZFMISC_1:29 ;
then reconsider m = [0,0] .--> (Funcs (0,0)) as ManySortedSet of [:1,1:] by PARTFUN1:def 2, RELAT_1:def 18;
A2: m . (0,0) = Funcs (0,0) by FUNCOP_1:72;
A3: 0 in 1 by CARD_1:49, 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:72;
then A6: dom ci = [:(m . (0,0)),(m . (0,0)):] by A2, PARTFUN1:def 2
.= {|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:4; :: thesis: verum

end;

then reconsider c = c as BinComp of m by PBOOLE:def 15;
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 13 :: 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:49, TARSKI:def 1;
A9: ( o1 = 0 & o2 = 0 ) by CARD_1:49, TARSKI:def 1;
then A10: dom (FuncComp ((Funcs (0,0)),(Funcs (0,0)))) = [:<^o2,o3^>,<^o1,o2^>:] by A2, A8, PARTFUN1:def 2;
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:72
.= (FuncComp ((Funcs (o1,o2)),(Funcs (o2,o3)))) | [:<^o2,o3^>,<^o1,o2^>:] by A9, A8, A10, RELAT_1:68 ; :: thesis: verum