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;
now for i being object st i in [:{0},{0},{0}:] holds
c . i is Function of ({|m,m|} . i),({|m|} . i)let i be
object ;
( 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}:]
;
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;
verum end;
then reconsider c = c as BinComp of m by PBOOLE:def 15;
take C = AltCatStr(# {0},m,c #); ( C is strict & C is pseudo-functional )
thus
C is strict
; C is pseudo-functional
let o1, o2, o3 be Object of C; ALTCAT_1:def 13 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
; verum