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
proof
let x,
y1,
y2 be
object ;
( [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 ) ) } implies y1 = y2 )
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 ) ) }
;
( not [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 ) ) } or y1 = y2 )
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 ) ) }
;
y1 = y2
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;
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 ;
( x in { [[n1,n2],n3] where n1, n2, n3 is Element of NAT : ( ( n1 <> n2 implies n3 = n1 + n2 ) & ( n1 = n2 implies n3 = 0 ) ) } implies x in [:[:NAT,NAT:],NAT:] )
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 ) ) }
;
x in [:[:NAT,NAT:],NAT:]
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;
verum
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
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 #);
( f1 = 0 implies ( f1 (*) f2 = f2 & f2 (*) f1 = f2 ) )
assume A11:
f1 = 0
;
( f1 (*) f2 = f2 & f2 (*) f1 = f2 )
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
;
f2 (*) f1 = f2
[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
;
verum
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 )
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 )
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 #);
for n1, n2 being Element of NAT st f1 = n1 & f2 = n2 & n1 = n2 holds
f1 (*) f2 = 0 let n1,
n2 be
Element of
NAT ;
( f1 = n1 & f2 = n2 & n1 = n2 implies f1 (*) f2 = 0 )
assume A23:
(
f1 = n1 &
f2 = n2 )
;
( not n1 = n2 or f1 (*) f2 = 0 )
assume A24:
n1 = n2
;
f1 (*) f2 = 0
[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
;
verum
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 #);
for n1, n2 being Element of NAT st f1 = n1 & f2 = n2 & n1 <> n2 holds
f1 (*) f2 = n1 + n2let n1,
n2 be
Element of
NAT ;
( f1 = n1 & f2 = n2 & n1 <> n2 implies f1 (*) f2 = n1 + n2 )
assume A29:
(
f1 = n1 &
f2 = n2 )
;
( not n1 <> n2 or f1 (*) f2 = n1 + n2 )
assume A30:
n1 <> n2
;
f1 (*) f2 = n1 + n2
[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
;
verum
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 )
hence
ex b1 being CategoryStr st
( not b1 is associative & b1 is composable & b1 is with_identities )
by A19, A21, Def10; verum