A1:
{[0,0,0]} = [:{0},{0},{0}:]
by MCART_1:35;

then reconsider c = [0,0,0] .--> (FuncComp ((Funcs (0,0)),(Funcs (0,0)))) as ManySortedSet of [:{0},{0},{0}:] ;

reconsider c = c as ManySortedFunction of [:{0},{0},{0}:] ;

dom ([0,0] .--> (Funcs (0,0))) = {[0,0]}

.= [:{0},{0}:] by ZFMISC_1:29 ;

then reconsider m = [0,0] .--> (Funcs (0,0)) as ManySortedSet of [:{0},{0}:] ;

A2: m . (0,0) = Funcs (0,0) by FUNCOP_1:72;

A3: 0 in {0} by TARSKI:def 1;

take C = AltCatStr(# {0},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 TARSKI:def 1;

A9: ( o1 = 0 & o2 = 0 ) by 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 ; :: thesis: verum

then reconsider c = [0,0,0] .--> (FuncComp ((Funcs (0,0)),(Funcs (0,0)))) as ManySortedSet of [:{0},{0},{0}:] ;

reconsider c = c as ManySortedFunction of [:{0},{0},{0}:] ;

dom ([0,0] .--> (Funcs (0,0))) = {[0,0]}

.= [:{0},{0}:] by ZFMISC_1:29 ;

then reconsider m = [0,0] .--> (Funcs (0,0)) as ManySortedSet of [:{0},{0}:] ;

A2: m . (0,0) = Funcs (0,0) by FUNCOP_1:72;

A3: 0 in {0} by TARSKI:def 1;

now :: thesis: for i being object st i in [:{0},{0},{0}:] 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 [:{0},{0},{0}:] implies c . i is Function of ({|m,m|} . i),({|m|} . i) )

reconsider ci = c . i as Function ;

assume i in [:{0},{0},{0}:] ; :: 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, Def4

.= {|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, Def3 ;

then rng ci c= {|m|} . i by A2, A5, Th6;

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;reconsider ci = c . i as Function ;

assume i in [:{0},{0},{0}:] ; :: 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, Def4

.= {|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, Def3 ;

then rng ci c= {|m|} . i by A2, A5, Th6;

hence c . i is Function of ({|m,m|} . i),({|m|} . i) by A2, A6, A7, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum

take C = AltCatStr(# {0},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 TARSKI:def 1;

A9: ( o1 = 0 & o2 = 0 ) by 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 ; :: thesis: verum