set X = NAT ;
set comp = { [[n1,n2],n3] where n1, n2, n3 is Element of NAT : ( ( n1 <> n2 implies n3 = n1 + n2 ) & ( n1 = n2 implies n3 = 0 ) ) } ;
A1: for x, y1, y2 being object st [x,y1] in { [[n1,n2],n3] where n1, n2, n3 is Element of NAT : ( ( n1 <> n2 implies n3 = n1 + n2 ) & ( n1 = n2 implies n3 = 0 ) ) } & [x,y2] in { [[n1,n2],n3] where n1, n2, n3 is Element of NAT : ( ( n1 <> n2 implies n3 = n1 + n2 ) & ( n1 = n2 implies n3 = 0 ) ) } holds
y1 = y2

let x, y1, y2 be object ; :: thesis:
assume [x,y1] in { [[n1,n2],n3] where n1, n2, n3 is Element of NAT : ( ( n1 <> n2 implies n3 = n1 + n2 ) & ( n1 = n2 implies n3 = 0 ) ) } ; :: thesis:
then consider n11, n12, n13 being Element of NAT such that
A2: ( [x,y1] = [[n11,n12],n13] & ( n11 <> n12 implies n13 = n11 + n12 ) & ( n11 = n12 implies n13 = 0 ) ) ;
assume [x,y2] in { [[n1,n2],n3] where n1, n2, n3 is Element of NAT : ( ( n1 <> n2 implies n3 = n1 + n2 ) & ( n1 = n2 implies n3 = 0 ) ) } ; :: thesis:
then consider n21, n22, n23 being Element of NAT such that
A3: ( [x,y2] = [[n21,n22],n23] & ( n21 <> n22 implies n23 = n21 + n22 ) & ( n21 = n22 implies n23 = 0 ) ) ;
A4: ( x = [n11,n12] & y1 = n13 ) by A2, XTUPLE_0:1;
( x = [n21,n22] & y2 = n23 ) by A3, XTUPLE_0:1;
then A5: ( n11 = n21 & n12 = n22 ) by A4, XTUPLE_0:1;

suppose n11 <> n12 ; :: thesis:

thus y1 = y2 by A2, A3, A5, XTUPLE_0:1; :: thesis:

end;

suppose n11 = n12 ; :: thesis:

thus y1 = y2 by A2, A3, A5, XTUPLE_0:1; :: thesis:

end;

for x being object st x in { [[n1,n2],n3] where n1, n2, n3 is Element of NAT : ( ( n1 <> n2 implies n3 = n1 + n2 ) & ( n1 = n2 implies n3 = 0 ) ) } holds
x in [:[:NAT,NAT:],NAT:]

proof

let x be object ; :: thesis:
assume x in { [[n1,n2],n3] where n1, n2, n3 is Element of NAT : ( ( n1 <> n2 implies n3 = n1 + n2 ) & ( n1 = n2 implies n3 = 0 ) ) } ; :: thesis:
then consider n11, n12, n13 being Element of NAT such that
A6: ( x = [[n11,n12],n13] & ( n11 <> n12 implies n13 = n11 + n12 ) & ( n11 = n12 implies n13 = 0 ) ) ;
[n11,n12] in [:NAT,NAT:] by ZFMISC_1:def 2;
hence x in [:[:NAT,NAT:],NAT:] by A6, ZFMISC_1:def 2; :: thesis:

end;

then reconsider comp = { [[n1,n2],n3] where n1, n2, n3 is Element of NAT : ( ( n1 <> n2 implies n3 = n1 + n2 ) & ( n1 = n2 implies n3 = 0 ) ) } as PartFunc of [:NAT,NAT:],NAT by A1, TARSKI:def 3, FUNCT_1:def 1;
set C = CategoryStr(# NAT,comp #);
A7: for f1, f2 being morphism of CategoryStr(# NAT,comp #) holds f1 |> f2

proof

let f1, f2 be morphism of CategoryStr(# NAT,comp #); :: thesis:
reconsider n1 = f1, n2 = f2 as Element of NAT ;

per cases ;

suppose A8: n1 <> n2 ; :: thesis:

reconsider n3 = n1 + n2 as Element of NAT ;
[[n1,n2],n3] in the composition of CategoryStr(# NAT,comp #) by A8;
hence f1 |> f2 by FUNCT_1:1; :: thesis:

end;

suppose A9: n1 = n2 ; :: thesis:

set n3 = 0 ;
[[n1,n2],0] in the composition of CategoryStr(# NAT,comp #) by A9;
hence f1 |> f2 by FUNCT_1:1; :: thesis:

end;

A10: for f1, f2 being morphism of CategoryStr(# NAT,comp #) st f1 = 0 holds
( f1 (*) f2 = f2 & f2 (*) f1 = f2 )

proof

let f1, f2 be morphism of CategoryStr(# NAT,comp #); :: thesis:
assume A11: f1 = 0 ; :: thesis:
reconsider n2 = f2 as Element of NAT ;
[f1,f2] in dom the composition of CategoryStr(# NAT,comp #) by A7, Def2;
then consider y being object such that
A12: [[f1,f2],y] in the composition of CategoryStr(# NAT,comp #) by XTUPLE_0:def 12;
consider n1, n2, n3 being Element of NAT such that
A13: ( [[f1,f2],y] = [[n1,n2],n3] & ( n1 <> n2 implies n3 = n1 + n2 ) & ( n1 = n2 implies n3 = 0 ) ) by A12;
( [f1,f2] = [n1,n2] & y = n3 ) by A13, XTUPLE_0:1;
then A14: ( f1 = n1 & f2 = n2 ) by XTUPLE_0:1;
thus f1 (*) f2 = the composition of CategoryStr(# NAT,comp #) . (f1,f2) by Def3, A7
.= the composition of CategoryStr(# NAT,comp #) . [f1,f2] by BINOP_1:def 1
.= f2 by FUNCT_1:1, A12, A13, A14, A11 ; :: thesis:
[f2,f1] in dom the composition of CategoryStr(# NAT,comp #) by A7, Def2;
then consider y being object such that
A15: [[f2,f1],y] in the composition of CategoryStr(# NAT,comp #) by XTUPLE_0:def 12;
consider n2, n1, n3 being Element of NAT such that
A16: ( [[f2,f1],y] = [[n2,n1],n3] & ( n2 <> n1 implies n3 = n2 + n1 ) & ( n2 = n1 implies n3 = 0 ) ) by A15;
( [f2,f1] = [n2,n1] & y = n3 ) by A16, XTUPLE_0:1;
then A17: ( f2 = n2 & f1 = n1 ) by XTUPLE_0:1;
thus f2 (*) f1 = the composition of CategoryStr(# NAT,comp #) . (f2,f1) by Def3, A7
.= the composition of CategoryStr(# NAT,comp #) . [f2,f1] by BINOP_1:def 1
.= f2 by FUNCT_1:1, A15, A16, A17, A11 ; :: thesis:

end;

A18: CategoryStr(# NAT,comp #) is left_composable by A7;
for f, f1, f2 being morphism of CategoryStr(# NAT,comp #) st f1 |> f2 holds
( f |> f1 (*) f2 iff f |> f1 ) by A7;
then A19: CategoryStr(# NAT,comp #) is composable by A18, Def9;
for f1 being morphism of CategoryStr(# NAT,comp #) st f1 in the carrier of CategoryStr(# NAT,comp #) holds
ex f being morphism of CategoryStr(# NAT,comp #) st
( f |> f1 & f is left_identity )

proof

let f1 be morphism of CategoryStr(# NAT,comp #); :: thesis:
assume f1 in the carrier of CategoryStr(# NAT,comp #) ; :: thesis:
reconsider f = 0 as morphism of CategoryStr(# NAT,comp #) ;
take f ; :: thesis:
thus f |> f1 by A7; :: thesis:
thus f is left_identity by A10; :: thesis:

end;

then A20: CategoryStr(# NAT,comp #) is with_left_identities ;
for f1 being morphism of CategoryStr(# NAT,comp #) st f1 in the carrier of CategoryStr(# NAT,comp #) holds
ex f being morphism of CategoryStr(# NAT,comp #) st
( f1 |> f & f is right_identity )

proof

let f1 be morphism of CategoryStr(# NAT,comp #); :: thesis:
assume f1 in the carrier of CategoryStr(# NAT,comp #) ; :: thesis:
reconsider f = 0 as morphism of CategoryStr(# NAT,comp #) ;
take f ; :: thesis:
thus f1 |> f by A7; :: thesis:
thus f is right_identity by A10; :: thesis:

end;

then A21: CategoryStr(# NAT,comp #) is with_identities by A20, Def7;
A22: for f1, f2 being morphism of CategoryStr(# NAT,comp #)
for n1, n2 being Element of NAT st f1 = n1 & f2 = n2 & n1 = n2 holds
f1 (*) f2 = 0

proof

let f1, f2 be morphism of CategoryStr(# NAT,comp #); :: thesis:
let n1, n2 be Element of NAT ; :: thesis:
assume A23: ( f1 = n1 & f2 = n2 ) ; :: thesis:
assume A24: n1 = n2 ; :: thesis:
[f1,f2] in dom the composition of CategoryStr(# NAT,comp #) by A7, Def2;
then consider y being object such that
A25: [[f1,f2],y] in the composition of CategoryStr(# NAT,comp #) by XTUPLE_0:def 12;
consider n11, n22, n33 being Element of NAT such that
A26: ( [[f1,f2],y] = [[n11,n22],n33] & ( n11 <> n22 implies n33 = n11 + n22 ) & ( n11 = n22 implies n33 = 0 ) ) by A25;
( [f1,f2] = [n11,n22] & y = n33 ) by A26, XTUPLE_0:1;
then A27: ( f1 = n11 & f2 = n22 ) by XTUPLE_0:1;
thus f1 (*) f2 = the composition of CategoryStr(# NAT,comp #) . (f1,f2) by Def3, A7
.= the composition of CategoryStr(# NAT,comp #) . [f1,f2] by BINOP_1:def 1
.= 0 by A27, FUNCT_1:1, A25, A26, A24, A23 ; :: thesis:

end;

A28: for f1, f2 being morphism of CategoryStr(# NAT,comp #)
for n1, n2 being Element of NAT st f1 = n1 & f2 = n2 & n1 <> n2 holds
f1 (*) f2 = n1 + n2

proof

let f1, f2 be morphism of CategoryStr(# NAT,comp #); :: thesis:
let n1, n2 be Element of NAT ; :: thesis:
assume A29: ( f1 = n1 & f2 = n2 ) ; :: thesis:
assume A30: n1 <> n2 ; :: thesis:
[f1,f2] in dom the composition of CategoryStr(# NAT,comp #) by A7, Def2;
then consider y being object such that
A31: [[f1,f2],y] in the composition of CategoryStr(# NAT,comp #) by XTUPLE_0:def 12;
consider n11, n22, n33 being Element of NAT such that
A32: ( [[f1,f2],y] = [[n11,n22],n33] & ( n11 <> n22 implies n33 = n11 + n22 ) & ( n11 = n22 implies n33 = 0 ) ) by A31;
( [f1,f2] = [n11,n22] & y = n33 ) by A32, XTUPLE_0:1;
then A33: ( f1 = n11 & f2 = n22 ) by XTUPLE_0:1;
thus f1 (*) f2 = the composition of CategoryStr(# NAT,comp #) . (f1,f2) by Def3, A7
.= the composition of CategoryStr(# NAT,comp #) . [f1,f2] by BINOP_1:def 1
.= n1 + n2 by A33, FUNCT_1:1, A31, A32, A30, A29 ; :: thesis:

end;

ex f1, f2, f3 being morphism of CategoryStr(# NAT,comp #) st
( f1 |> f2 & f2 |> f3 & f1 (*) f2 |> f3 & f1 |> f2 (*) f3 & not f1 (*) (f2 (*) f3) = (f1 (*) f2) (*) f3 )

proof

reconsider f1 = 1, f2 = 2, f3 = 3 as morphism of CategoryStr(# NAT,comp #) ;
take f1 ; :: thesis:
take f2 ; :: thesis:
take f3 ; :: thesis:
thus ( f1 |> f2 & f2 |> f3 & f1 (*) f2 |> f3 & f1 |> f2 (*) f3 ) by A7; :: thesis:
A34: ( f1 (*) f2 = 1 + 2 & f2 (*) f3 = 2 + 3 ) by A28;
reconsider f12 = 3, f23 = 5 as morphism of CategoryStr(# NAT,comp #) ;
( f1 (*) f23 = 1 + 5 & f12 (*) f3 = 0 ) by A22, A28;
hence not f1 (*) (f2 (*) f3) = (f1 (*) f2) (*) f3 by A34; :: thesis:

end;

hence ex b₁ being CategoryStr st
( not b₁ is associative & b₁ is composable & b₁ is with_identities ) by A19, A21, Def10; :: thesis: