set X1 = NAT \ {0};
set X2 = { [n1,n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ;
reconsider X = (NAT \ {0}) \/ { [n1,n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } as set ;
set c0 = { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } ;
set c1 = { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ;
set c2 = { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } ;
set c3 = { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } ;
set comp = (( { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } \/ { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ) \/ { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } ) \/ { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } ;
( 1 in NAT & not 1 in {0} )
by TARSKI:def 1;
then A1:
1 in NAT \ {0}
by XBOOLE_0:def 5;
A2:
for x, y1, y2 being object st [x,y1] in (( { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } \/ { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ) \/ { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } ) \/ { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } & [x,y2] in (( { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } \/ { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ) \/ { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } ) \/ { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } holds
y1 = y2
proof
let x,
y1,
y2 be
object ;
( [x,y1] in (( { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } \/ { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ) \/ { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } ) \/ { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } & [x,y2] in (( { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } \/ { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ) \/ { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } ) \/ { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } implies y1 = y2 )
assume
[x,y1] in (( { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } \/ { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ) \/ { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } ) \/ { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) }
;
( not [x,y2] in (( { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } \/ { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ) \/ { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } ) \/ { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } or y1 = y2 )
then
(
[x,y1] in ( { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } \/ { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ) \/ { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } or
[x,y1] in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } )
by XBOOLE_0:def 3;
then A3:
(
[x,y1] in { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } \/ { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } or
[x,y1] in { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } or
[x,y1] in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } )
by XBOOLE_0:def 3;
assume
[x,y2] in (( { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } \/ { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ) \/ { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } ) \/ { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) }
;
y1 = y2
then
(
[x,y2] in ( { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } \/ { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ) \/ { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } or
[x,y2] in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } )
by XBOOLE_0:def 3;
then A4:
(
[x,y2] in { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } \/ { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } or
[x,y2] in { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } or
[x,y2] in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } )
by XBOOLE_0:def 3;
per cases
( [x,y1] in { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } or [x,y1] in { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } or [x,y1] in { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } or [x,y1] in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } )
by A3, XBOOLE_0:def 3;
suppose
[x,y1] in { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 }
;
y1 = y2then consider n11,
n12 being
Element of
NAT such that A5:
(
[x,y1] = [[[n11,n12],[n11,n12]],[n11,n12]] &
n12 = n11 + 1 )
;
A6:
(
x = [[n11,n12],[n11,n12]] &
y1 = [n11,n12] )
by A5, XTUPLE_0:1;
per cases
( [x,y2] in { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } or [x,y2] in { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } or [x,y2] in { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } or [x,y2] in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } )
by A4, XBOOLE_0:def 3;
suppose
[x,y2] in { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 }
;
y1 = y2then consider n21,
n22 being
Element of
NAT such that A7:
(
[x,y2] = [[[n21,n22],[n21,n22]],[n21,n22]] &
n22 = n21 + 1 )
;
(
x = [[n21,n22],[n21,n22]] &
y2 = [n21,n22] )
by A7, XTUPLE_0:1;
hence
y1 = y2
by A6, XTUPLE_0:1;
verum end; end; end; suppose
[x,y1] in { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 }
;
y1 = y2then consider n11,
n12 being
Element of
NAT such that A11:
(
[x,y1] = [[[n11,n12],n12],n12] &
n12 = n11 + 1 )
;
A12:
(
x = [[n11,n12],n12] &
y1 = n12 )
by A11, XTUPLE_0:1;
per cases
( [x,y2] in { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } or [x,y2] in { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } or [x,y2] in { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } or [x,y2] in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } )
by A4, XBOOLE_0:def 3;
suppose
[x,y2] in { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 }
;
y1 = y2then consider n21,
n22 being
Element of
NAT such that A13:
(
[x,y2] = [[[n21,n22],[n21,n22]],[n21,n22]] &
n22 = n21 + 1 )
;
(
x = [[n21,n22],[n21,n22]] &
y2 = [n21,n22] )
by A13, XTUPLE_0:1;
hence
y1 = y2
by A12, XTUPLE_0:1;
verum end; end; end; suppose
[x,y1] in { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) }
;
y1 = y2then consider n11,
n12 being
Element of
NAT such that A17:
(
[x,y1] = [[n11,[n11,n12]],n11] &
n12 = n11 + 1 &
n11 <> 0 )
;
A18:
(
x = [n11,[n11,n12]] &
y1 = n11 )
by A17, XTUPLE_0:1;
per cases
( [x,y2] in { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } or [x,y2] in { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } or [x,y2] in { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } or [x,y2] in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } )
by A4, XBOOLE_0:def 3;
suppose
[x,y2] in { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 }
;
y1 = y2then consider n21,
n22 being
Element of
NAT such that A19:
(
[x,y2] = [[[n21,n22],[n21,n22]],[n21,n22]] &
n22 = n21 + 1 )
;
(
x = [[n21,n22],[n21,n22]] &
y2 = [n21,n22] )
by A19, XTUPLE_0:1;
hence
y1 = y2
by A18, XTUPLE_0:1;
verum end; end; end; suppose
[x,y1] in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) }
;
y1 = y2then consider n11,
n12 being
Element of
NAT such that A23:
(
[x,y1] = [[n11,n12],n11] &
n12 = n11 + 1 &
n11 <> 0 )
;
A24:
(
x = [n11,n12] &
y1 = n11 )
by A23, XTUPLE_0:1;
per cases
( [x,y2] in { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } or [x,y2] in { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } or [x,y2] in { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } or [x,y2] in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } )
by A4, XBOOLE_0:def 3;
suppose
[x,y2] in { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 }
;
y1 = y2then consider n21,
n22 being
Element of
NAT such that A25:
(
[x,y2] = [[[n21,n22],[n21,n22]],[n21,n22]] &
n22 = n21 + 1 )
;
(
x = [[n21,n22],[n21,n22]] &
y2 = [n21,n22] )
by A25, XTUPLE_0:1;
hence
y1 = y2
by A24, XTUPLE_0:1;
verum end; end; end; end;
end;
for x being object st x in (( { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } \/ { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ) \/ { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } ) \/ { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } holds
x in [:[:X,X:],X:]
proof
let x be
object ;
( x in (( { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } \/ { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ) \/ { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } ) \/ { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } implies x in [:[:X,X:],X:] )
assume
x in (( { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } \/ { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ) \/ { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } ) \/ { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) }
;
x in [:[:X,X:],X:]
then
(
x in ( { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } \/ { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ) \/ { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } or
x in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } )
by XBOOLE_0:def 3;
then A29:
(
x in { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } \/ { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } or
x in { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } or
x in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } )
by XBOOLE_0:def 3;
per cases
( x in { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } or x in { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } or x in { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } or x in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } )
by A29, XBOOLE_0:def 3;
suppose
x in { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 }
;
x in [:[:X,X:],X:]then consider n1,
n2 being
Element of
NAT such that A30:
(
x = [[[n1,n2],[n1,n2]],[n1,n2]] &
n2 = n1 + 1 )
;
[n1,n2] in { [n1,n2] where n1, n2 is Element of NAT : n2 = n1 + 1 }
by A30;
then A31:
[n1,n2] in X
by XBOOLE_0:def 3;
then
[[n1,n2],[n1,n2]] in [:X,X:]
by ZFMISC_1:def 2;
hence
x in [:[:X,X:],X:]
by A30, A31, ZFMISC_1:def 2;
verum end; suppose
x in { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 }
;
x in [:[:X,X:],X:]then consider n1,
n2 being
Element of
NAT such that A32:
(
x = [[[n1,n2],n2],n2] &
n2 = n1 + 1 )
;
[n1,n2] in { [n1,n2] where n1, n2 is Element of NAT : n2 = n1 + 1 }
by A32;
then A33:
[n1,n2] in X
by XBOOLE_0:def 3;
not
n2 in {0}
by A32, TARSKI:def 1;
then
n2 in NAT \ {0}
by XBOOLE_0:def 5;
then A34:
n2 in X
by XBOOLE_0:def 3;
[[n1,n2],n2] in [:X,X:]
by A33, A34, ZFMISC_1:def 2;
hence
x in [:[:X,X:],X:]
by A32, A34, ZFMISC_1:def 2;
verum end; suppose
x in { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) }
;
x in [:[:X,X:],X:]then consider n1,
n2 being
Element of
NAT such that A35:
(
x = [[n1,[n1,n2]],n1] &
n2 = n1 + 1 &
n1 <> 0 )
;
[n1,n2] in { [n1,n2] where n1, n2 is Element of NAT : n2 = n1 + 1 }
by A35;
then A36:
[n1,n2] in X
by XBOOLE_0:def 3;
not
n1 in {0}
by A35, TARSKI:def 1;
then
n1 in NAT \ {0}
by XBOOLE_0:def 5;
then A37:
n1 in X
by XBOOLE_0:def 3;
[n1,[n1,n2]] in [:X,X:]
by A36, A37, ZFMISC_1:def 2;
hence
x in [:[:X,X:],X:]
by A35, A37, ZFMISC_1:def 2;
verum end; suppose
x in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) }
;
x in [:[:X,X:],X:]then consider n1,
n2 being
Element of
NAT such that A38:
(
x = [[n1,n2],n1] &
n2 = n1 + 1 &
n1 <> 0 )
;
not
n1 in {0}
by A38, TARSKI:def 1;
then
n1 in NAT \ {0}
by XBOOLE_0:def 5;
then A39:
n1 in X
by XBOOLE_0:def 3;
not
n2 in {0}
by A38, TARSKI:def 1;
then
n2 in NAT \ {0}
by XBOOLE_0:def 5;
then A40:
n2 in X
by XBOOLE_0:def 3;
[n1,n2] in [:X,X:]
by A39, A40, ZFMISC_1:def 2;
hence
x in [:[:X,X:],X:]
by A38, A39, ZFMISC_1:def 2;
verum end; end;
end;
then reconsider comp = (( { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } \/ { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ) \/ { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } ) \/ { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } as PartFunc of [:X,X:],X by A2, TARSKI:def 3, FUNCT_1:def 1;
set C = CategoryStr(# X,comp #);
A41:
for n1 being Element of NAT st n1 <> 0 holds
n1 is morphism of CategoryStr(# X,comp #)
A42:
for f1, f2 being morphism of CategoryStr(# X,comp #)
for n1, n2 being Element of NAT st f1 = n1 & f2 = n2 & n2 = n1 + 1 & n1 <> 0 holds
( f1 |> f2 & f1 (*) f2 = f1 )
proof
let f1,
f2 be
morphism of
CategoryStr(#
X,
comp #);
for n1, n2 being Element of NAT st f1 = n1 & f2 = n2 & n2 = n1 + 1 & n1 <> 0 holds
( f1 |> f2 & f1 (*) f2 = f1 )let n1,
n2 be
Element of
NAT ;
( f1 = n1 & f2 = n2 & n2 = n1 + 1 & n1 <> 0 implies ( f1 |> f2 & f1 (*) f2 = f1 ) )
assume A43:
(
f1 = n1 &
f2 = n2 )
;
( not n2 = n1 + 1 or not n1 <> 0 or ( f1 |> f2 & f1 (*) f2 = f1 ) )
assume
(
n2 = n1 + 1 &
n1 <> 0 )
;
( f1 |> f2 & f1 (*) f2 = f1 )
then A44:
[[n1,n2],n1] in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) }
;
then A45:
[[n1,n2],n1] in (( { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } \/ { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ) \/ { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } ) \/ { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) }
by XBOOLE_0:def 3;
A46:
[[n1,n2],n1] in the
composition of
CategoryStr(#
X,
comp #)
by A44, XBOOLE_0:def 3;
A47:
[f1,f2] in dom the
composition of
CategoryStr(#
X,
comp #)
by A43, A45, XTUPLE_0:def 12;
thus
f1 |> f2
by A43, A45, XTUPLE_0:def 12;
f1 (*) f2 = f1
thus f1 (*) f2 =
the
composition of
CategoryStr(#
X,
comp #)
. (
f1,
f2)
by A47, Def2, Def3
.=
the
composition of
CategoryStr(#
X,
comp #)
. [n1,n2]
by A43, BINOP_1:def 1
.=
f1
by A46, A43, FUNCT_1:1
;
verum
end;
A48:
for f being morphism of CategoryStr(# X,comp #) st f in { [n1,n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } holds
( f is left_identity & f is right_identity & f |> f )
proof
let f be
morphism of
CategoryStr(#
X,
comp #);
( f in { [n1,n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } implies ( f is left_identity & f is right_identity & f |> f ) )
assume
f in { [n1,n2] where n1, n2 is Element of NAT : n2 = n1 + 1 }
;
( f is left_identity & f is right_identity & f |> f )
then consider nf1,
nf2 being
Element of
NAT such that A49:
(
f = [nf1,nf2] &
nf2 = nf1 + 1 )
;
for
f1 being
morphism of
CategoryStr(#
X,
comp #) st
f |> f1 holds
f (*) f1 = f1
proof
let f1 be
morphism of
CategoryStr(#
X,
comp #);
( f |> f1 implies f (*) f1 = f1 )
assume A50:
f |> f1
;
f (*) f1 = f1
then consider y being
object such that A51:
[[f,f1],y] in the
composition of
CategoryStr(#
X,
comp #)
by XTUPLE_0:def 12;
(
[[f,f1],y] in ( { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } \/ { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ) \/ { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } or
[[f,f1],y] in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } )
by A51, XBOOLE_0:def 3;
then A52:
(
[[f,f1],y] in { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } \/ { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } or
[[f,f1],y] in { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } or
[[f,f1],y] in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } )
by XBOOLE_0:def 3;
per cases
( [[f,f1],y] in { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } or [[f,f1],y] in { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } or [[f,f1],y] in { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } or [[f,f1],y] in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } )
by A52, XBOOLE_0:def 3;
suppose
[[f,f1],y] in { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 }
;
f (*) f1 = f1then consider n1,
n2 being
Element of
NAT such that A53:
(
[[f,f1],y] = [[[n1,n2],[n1,n2]],[n1,n2]] &
n2 = n1 + 1 )
;
(
[f,f1] = [[n1,n2],[n1,n2]] &
y = [n1,n2] )
by A53, XTUPLE_0:1;
then A54:
(
f = [n1,n2] &
f1 = [n1,n2] )
by XTUPLE_0:1;
thus f (*) f1 =
the
composition of
CategoryStr(#
X,
comp #)
. (
f,
f1)
by A50, Def3
.=
the
composition of
CategoryStr(#
X,
comp #)
. [f,f1]
by BINOP_1:def 1
.=
f1
by A54, A51, FUNCT_1:1, A53
;
verum end; suppose
[[f,f1],y] in { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 }
;
f (*) f1 = f1then consider n1,
n2 being
Element of
NAT such that A55:
(
[[f,f1],y] = [[[n1,n2],n2],n2] &
n2 = n1 + 1 )
;
(
[f,f1] = [[n1,n2],n2] &
y = n2 )
by A55, XTUPLE_0:1;
then A56:
(
f = [n1,n2] &
f1 = n2 )
by XTUPLE_0:1;
thus f (*) f1 =
the
composition of
CategoryStr(#
X,
comp #)
. (
f,
f1)
by A50, Def3
.=
the
composition of
CategoryStr(#
X,
comp #)
. [f,f1]
by BINOP_1:def 1
.=
f1
by A56, A51, FUNCT_1:1, A55
;
verum end; suppose
[[f,f1],y] in { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) }
;
f (*) f1 = f1then consider n1,
n2 being
Element of
NAT such that A57:
(
[[f,f1],y] = [[n1,[n1,n2]],n1] &
n2 = n1 + 1 &
n1 <> 0 )
;
[f,f1] = [n1,[n1,n2]]
by A57, XTUPLE_0:1;
hence
f (*) f1 = f1
by A49, XTUPLE_0:1;
verum end; end;
end;
hence
f is
left_identity
;
( f is right_identity & f |> f )
for
f1 being
morphism of
CategoryStr(#
X,
comp #) st
f1 |> f holds
f1 (*) f = f1
proof
let f1 be
morphism of
CategoryStr(#
X,
comp #);
( f1 |> f implies f1 (*) f = f1 )
assume A59:
f1 |> f
;
f1 (*) f = f1
then consider y being
object such that A60:
[[f1,f],y] in the
composition of
CategoryStr(#
X,
comp #)
by XTUPLE_0:def 12;
(
[[f1,f],y] in ( { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } \/ { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ) \/ { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } or
[[f1,f],y] in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } )
by A60, XBOOLE_0:def 3;
then A61:
(
[[f1,f],y] in { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } \/ { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } or
[[f1,f],y] in { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } or
[[f1,f],y] in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } )
by XBOOLE_0:def 3;
per cases
( [[f1,f],y] in { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } or [[f1,f],y] in { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } or [[f1,f],y] in { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } or [[f1,f],y] in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } )
by A61, XBOOLE_0:def 3;
suppose
[[f1,f],y] in { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 }
;
f1 (*) f = f1then consider n1,
n2 being
Element of
NAT such that A62:
(
[[f1,f],y] = [[[n1,n2],[n1,n2]],[n1,n2]] &
n2 = n1 + 1 )
;
(
[f1,f] = [[n1,n2],[n1,n2]] &
y = [n1,n2] )
by A62, XTUPLE_0:1;
then A63:
(
f1 = [n1,n2] &
f = [n1,n2] )
by XTUPLE_0:1;
thus f1 (*) f =
the
composition of
CategoryStr(#
X,
comp #)
. (
f1,
f)
by A59, Def3
.=
the
composition of
CategoryStr(#
X,
comp #)
. [f1,f]
by BINOP_1:def 1
.=
f1
by A63, A60, FUNCT_1:1, A62
;
verum end; suppose
[[f1,f],y] in { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 }
;
f1 (*) f = f1then consider n1,
n2 being
Element of
NAT such that A64:
(
[[f1,f],y] = [[[n1,n2],n2],n2] &
n2 = n1 + 1 )
;
(
[f1,f] = [[n1,n2],n2] &
y = n2 )
by A64, XTUPLE_0:1;
hence
f1 (*) f = f1
by A49, XTUPLE_0:1;
verum end; suppose
[[f1,f],y] in { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) }
;
f1 (*) f = f1then consider n1,
n2 being
Element of
NAT such that A65:
(
[[f1,f],y] = [[n1,[n1,n2]],n1] &
n2 = n1 + 1 &
n1 <> 0 )
;
(
[f1,f] = [n1,[n1,n2]] &
y = n1 )
by A65, XTUPLE_0:1;
then A66:
(
f1 = n1 &
f = [n1,n2] )
by XTUPLE_0:1;
thus f1 (*) f =
the
composition of
CategoryStr(#
X,
comp #)
. (
f1,
f)
by A59, Def3
.=
the
composition of
CategoryStr(#
X,
comp #)
. [f1,f]
by BINOP_1:def 1
.=
f1
by A66, A60, FUNCT_1:1, A65
;
verum end; end;
end;
hence
f is
right_identity
;
f |> f
[[f,f],f] in { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 }
by A49;
then
[[f,f],f] in { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } \/ { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 }
by XBOOLE_0:def 3;
then
[[f,f],f] in ( { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } \/ { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ) \/ { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) }
by XBOOLE_0:def 3;
then
[[f,f],f] in (( { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } \/ { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ) \/ { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } ) \/ { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) }
by XBOOLE_0:def 3;
hence
f |> f
by FUNCT_1:1;
verum
end;
A68:
for f1, f2 being morphism of CategoryStr(# X,comp #) st f1 in NAT \ {0} & f1 |> f2 holds
f1 (*) f2 = f1
proof
let f1,
f2 be
morphism of
CategoryStr(#
X,
comp #);
( f1 in NAT \ {0} & f1 |> f2 implies f1 (*) f2 = f1 )
assume A69:
f1 in NAT \ {0}
;
( not f1 |> f2 or f1 (*) f2 = f1 )
reconsider nf1 =
f1 as
Element of
NAT by A69;
assume A70:
f1 |> f2
;
f1 (*) f2 = f1
per cases
( f2 in NAT \ {0} or f2 in { [n1,n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } )
by A1, XBOOLE_0:def 3;
suppose A71:
f2 in NAT \ {0}
;
f1 (*) f2 = f1reconsider nf2 =
f2 as
Element of
NAT by A71;
consider y being
object such that A72:
[[f1,f2],y] in the
composition of
CategoryStr(#
X,
comp #)
by A70, XTUPLE_0:def 12;
(
[[f1,f2],y] in ( { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } \/ { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ) \/ { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } or
[[f1,f2],y] in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } )
by A72, XBOOLE_0:def 3;
then A73:
(
[[f1,f2],y] in { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } \/ { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } or
[[f1,f2],y] in { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } or
[[f1,f2],y] in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } )
by XBOOLE_0:def 3;
per cases
( [[f1,f2],y] in { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } or [[f1,f2],y] in { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } or [[f1,f2],y] in { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } or [[f1,f2],y] in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } )
by A73, XBOOLE_0:def 3;
suppose
[[f1,f2],y] in { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 }
;
f1 (*) f2 = f1then consider n1,
n2 being
Element of
NAT such that A74:
(
[[f1,f2],y] = [[[n1,n2],[n1,n2]],[n1,n2]] &
n2 = n1 + 1 )
;
[f1,f2] = [[n1,n2],[n1,n2]]
by A74, XTUPLE_0:1;
hence
f1 (*) f2 = f1
by A71, XTUPLE_0:1;
verum end; suppose
[[f1,f2],y] in { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 }
;
f1 (*) f2 = f1then consider n1,
n2 being
Element of
NAT such that A75:
(
[[f1,f2],y] = [[[n1,n2],n2],n2] &
n2 = n1 + 1 )
;
(
[f1,f2] = [[n1,n2],n2] &
y = n2 )
by A75, XTUPLE_0:1;
hence
f1 (*) f2 = f1
by A69, XTUPLE_0:1;
verum end; suppose
[[f1,f2],y] in { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) }
;
f1 (*) f2 = f1then consider n1,
n2 being
Element of
NAT such that A76:
(
[[f1,f2],y] = [[n1,[n1,n2]],n1] &
n2 = n1 + 1 &
n1 <> 0 )
;
[f1,f2] = [n1,[n1,n2]]
by A76, XTUPLE_0:1;
hence
f1 (*) f2 = f1
by A71, XTUPLE_0:1;
verum end; suppose
[[f1,f2],y] in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) }
;
f1 (*) f2 = f1then consider n1,
n2 being
Element of
NAT such that A77:
(
[[f1,f2],y] = [[n1,n2],n1] &
n2 = n1 + 1 &
n1 <> 0 )
;
(
[f1,f2] = [n1,n2] &
y = n1 )
by A77, XTUPLE_0:1;
then A78:
(
f1 = n1 &
f2 = n2 )
by XTUPLE_0:1;
thus f1 (*) f2 =
the
composition of
CategoryStr(#
X,
comp #)
. (
f1,
f2)
by A70, Def3
.=
the
composition of
CategoryStr(#
X,
comp #)
. [f1,f2]
by BINOP_1:def 1
.=
f1
by A78, A72, FUNCT_1:1, A77
;
verum end; end; end; end;
end;
ex f, f1, f2 being morphism of CategoryStr(# X,comp #) st
( f1 |> f2 & ( ( f1 (*) f2 |> f & not f2 |> f ) or ( f2 |> f & not f1 (*) f2 |> f ) ) )
proof
reconsider f1 = 1,
f2 = 2,
f = 3 as
morphism of
CategoryStr(#
X,
comp #)
by A41;
take
f
;
ex f1, f2 being morphism of CategoryStr(# X,comp #) st
( f1 |> f2 & ( ( f1 (*) f2 |> f & not f2 |> f ) or ( f2 |> f & not f1 (*) f2 |> f ) ) )
take
f1
;
ex f2 being morphism of CategoryStr(# X,comp #) st
( f1 |> f2 & ( ( f1 (*) f2 |> f & not f2 |> f ) or ( f2 |> f & not f1 (*) f2 |> f ) ) )
take
f2
;
( f1 |> f2 & ( ( f1 (*) f2 |> f & not f2 |> f ) or ( f2 |> f & not f1 (*) f2 |> f ) ) )
A79:
2
= 1
+ 1
;
hence
f1 |> f2
by A42;
( ( f1 (*) f2 |> f & not f2 |> f ) or ( f2 |> f & not f1 (*) f2 |> f ) )
A80:
not
f1 |> f
proof
assume
f1 |> f
;
contradiction
then consider y being
object such that A81:
[[f1,f],y] in the
composition of
CategoryStr(#
X,
comp #)
by XTUPLE_0:def 12;
(
[[f1,f],y] in ( { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } \/ { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ) \/ { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } or
[[f1,f],y] in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } )
by A81, XBOOLE_0:def 3;
then A82:
(
[[f1,f],y] in { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } \/ { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } or
[[f1,f],y] in { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } or
[[f1,f],y] in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } )
by XBOOLE_0:def 3;
per cases
( [[f1,f],y] in { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } or [[f1,f],y] in { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } or [[f1,f],y] in { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } or [[f1,f],y] in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } )
by A82, XBOOLE_0:def 3;
suppose
[[f1,f],y] in { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 }
;
contradictionthen consider n1,
n2 being
Element of
NAT such that A83:
(
[[f1,f],y] = [[[n1,n2],[n1,n2]],[n1,n2]] &
n2 = n1 + 1 )
;
[f1,f] = [[n1,n2],[n1,n2]]
by A83, XTUPLE_0:1;
hence
contradiction
by XTUPLE_0:1;
verum end; suppose
[[f1,f],y] in { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 }
;
contradictionthen consider n1,
n2 being
Element of
NAT such that A84:
(
[[f1,f],y] = [[[n1,n2],n2],n2] &
n2 = n1 + 1 )
;
[f1,f] = [[n1,n2],n2]
by A84, XTUPLE_0:1;
hence
contradiction
by XTUPLE_0:1;
verum end; suppose
[[f1,f],y] in { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) }
;
contradictionthen consider n1,
n2 being
Element of
NAT such that A85:
(
[[f1,f],y] = [[n1,[n1,n2]],n1] &
n2 = n1 + 1 &
n1 <> 0 )
;
[f1,f] = [n1,[n1,n2]]
by A85, XTUPLE_0:1;
hence
contradiction
by XTUPLE_0:1;
verum end; end;
end;
3
= 2
+ 1
;
hence
( (
f1 (*) f2 |> f & not
f2 |> f ) or (
f2 |> f & not
f1 (*) f2 |> f ) )
by A42, A80, A79;
verum
end;
then A87:
not CategoryStr(# X,comp #) is left_composable
;
for f, f1, f2 being morphism of CategoryStr(# X,comp #) st f1 |> f2 holds
( f |> f1 (*) f2 iff f |> f1 )
proof
let f,
f1,
f2 be
morphism of
CategoryStr(#
X,
comp #);
( f1 |> f2 implies ( f |> f1 (*) f2 iff f |> f1 ) )
assume A88:
f1 |> f2
;
( f |> f1 (*) f2 iff f |> f1 )
per cases
( f2 in NAT \ {0} or f2 in { [n1,n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } )
by A1, XBOOLE_0:def 3;
suppose A89:
f2 in NAT \ {0}
;
( f |> f1 (*) f2 iff f |> f1 )per cases
( f1 in NAT \ {0} or f1 in { [n1,n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } )
by A1, XBOOLE_0:def 3;
suppose A90:
f1 in { [n1,n2] where n1, n2 is Element of NAT : n2 = n1 + 1 }
;
( f |> f1 (*) f2 iff f |> f1 )then A91:
f1 is
left_identity
by A48;
then A92:
f1 (*) f2 = f2
by A88;
consider n1,
n2 being
Element of
NAT such that A93:
(
f1 = [n1,n2] &
n2 = n1 + 1 )
by A90;
reconsider n3 =
f2 as
Element of
NAT by A89;
A94:
n2 = n3
proof
assume A95:
n2 <> n3
;
contradiction
consider y being
object such that A96:
[[f1,f2],y] in the
composition of
CategoryStr(#
X,
comp #)
by A88, XTUPLE_0:def 12;
(
[[f1,f2],y] in ( { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } \/ { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ) \/ { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } or
[[f1,f2],y] in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } )
by A96, XBOOLE_0:def 3;
then A97:
(
[[f1,f2],y] in { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } \/ { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } or
[[f1,f2],y] in { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } or
[[f1,f2],y] in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } )
by XBOOLE_0:def 3;
per cases
( [[f1,f2],y] in { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } or [[f1,f2],y] in { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } or [[f1,f2],y] in { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } or [[f1,f2],y] in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } )
by A97, XBOOLE_0:def 3;
suppose
[[f1,f2],y] in { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 }
;
contradictionthen consider n1,
n2 being
Element of
NAT such that A98:
(
[[f1,f2],y] = [[[n1,n2],[n1,n2]],[n1,n2]] &
n2 = n1 + 1 )
;
[f1,f2] = [[n1,n2],[n1,n2]]
by A98, XTUPLE_0:1;
hence
contradiction
by XTUPLE_0:1, A89;
verum end; suppose
[[f1,f2],y] in { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 }
;
contradictionthen consider n11,
n22 being
Element of
NAT such that A99:
(
[[f1,f2],y] = [[[n11,n22],n22],n22] &
n22 = n11 + 1 )
;
[f1,f2] = [[n11,n22],n22]
by A99, XTUPLE_0:1;
then
(
f1 = [n11,n22] &
f2 = n22 )
by XTUPLE_0:1;
hence
contradiction
by A95, A93, XTUPLE_0:1;
verum end; suppose
[[f1,f2],y] in { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) }
;
contradictionthen consider n1,
n2 being
Element of
NAT such that A100:
(
[[f1,f2],y] = [[n1,[n1,n2]],n1] &
n2 = n1 + 1 &
n1 <> 0 )
;
[f1,f2] = [n1,[n1,n2]]
by A100, XTUPLE_0:1;
hence
contradiction
by XTUPLE_0:1, A89;
verum end; end;
end; hereby ( f |> f1 implies f |> f1 (*) f2 )
assume
f |> f1 (*) f2
;
f |> f1then consider y being
object such that A102:
[[f,f2],y] in the
composition of
CategoryStr(#
X,
comp #)
by A92, XTUPLE_0:def 12;
(
[[f,f2],y] in ( { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } \/ { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ) \/ { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } or
[[f,f2],y] in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } )
by A102, XBOOLE_0:def 3;
then A103:
(
[[f,f2],y] in { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } \/ { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } or
[[f,f2],y] in { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } or
[[f,f2],y] in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } )
by XBOOLE_0:def 3;
per cases
( [[f,f2],y] in { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } or [[f,f2],y] in { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } or [[f,f2],y] in { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } or [[f,f2],y] in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } )
by A103, XBOOLE_0:def 3;
suppose
[[f,f2],y] in { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 }
;
f |> f1then consider n,
n2 being
Element of
NAT such that A104:
(
[[f,f2],y] = [[[n,n2],[n,n2]],[n,n2]] &
n2 = n + 1 )
;
[f,f2] = [[n,n2],[n,n2]]
by A104, XTUPLE_0:1;
hence
f |> f1
by XTUPLE_0:1, A89;
verum end; suppose
[[f,f2],y] in { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 }
;
f |> f1then consider n,
n22 being
Element of
NAT such that A105:
(
[[f,f2],y] = [[[n,n22],n22],n22] &
n22 = n + 1 )
;
[f,f2] = [[n,n22],n22]
by A105, XTUPLE_0:1;
then A106:
(
f = [n,n22] &
f2 = n22 )
by XTUPLE_0:1;
[[f1,f1],f1] in { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 }
by A93;
then
[[f1,f1],f1] in { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } \/ { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 }
by XBOOLE_0:def 3;
then
[[f1,f1],f1] in ( { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } \/ { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ) \/ { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) }
by XBOOLE_0:def 3;
then
[[f1,f1],f1] in the
composition of
CategoryStr(#
X,
comp #)
by XBOOLE_0:def 3;
hence
f |> f1
by A93, A106, A105, A94, XTUPLE_0:def 12;
verum end; suppose
[[f,f2],y] in { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) }
;
f |> f1then consider n,
n2 being
Element of
NAT such that A107:
(
[[f,f2],y] = [[n,[n,n2]],n] &
n2 = n + 1 &
n <> 0 )
;
[f,f2] = [n,[n,n2]]
by A107, XTUPLE_0:1;
hence
f |> f1
by A89, XTUPLE_0:1;
verum end; suppose
[[f,f2],y] in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) }
;
f |> f1then consider n,
n22 being
Element of
NAT such that A108:
(
[[f,f2],y] = [[n,n22],n] &
n22 = n + 1 &
n <> 0 )
;
A109:
[f,f2] = [n,n22]
by A108, XTUPLE_0:1;
then A110:
(
f = n &
f2 = n22 )
by XTUPLE_0:1;
A111:
n + 1
= n1 + 1
by A94, A108, A93, A109, XTUPLE_0:1;
[[n1,[n1,n2]],n1] in { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) }
by A93, A108, A111;
then
[[f,f1],f] in ( { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } \/ { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ) \/ { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) }
by A93, A110, XBOOLE_0:def 3, A94, A108;
then
[[f,f1],f] in the
composition of
CategoryStr(#
X,
comp #)
by XBOOLE_0:def 3;
hence
f |> f1
by XTUPLE_0:def 12;
verum end; end;
end; assume A112:
f |> f1
;
f |> f1 (*) f2
f |> f2
proof
consider y being
object such that A113:
[[f,f1],y] in the
composition of
CategoryStr(#
X,
comp #)
by A112, XTUPLE_0:def 12;
(
[[f,f1],y] in ( { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } \/ { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ) \/ { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } or
[[f,f1],y] in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } )
by A113, XBOOLE_0:def 3;
then A114:
(
[[f,f1],y] in { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } \/ { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } or
[[f,f1],y] in { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } or
[[f,f1],y] in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } )
by XBOOLE_0:def 3;
per cases
( [[f,f1],y] in { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } or [[f,f1],y] in { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } or [[f,f1],y] in { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } or [[f,f1],y] in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } )
by A114, XBOOLE_0:def 3;
suppose
[[f,f1],y] in { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 }
;
f |> f2then consider n,
n1 being
Element of
NAT such that A115:
(
[[f,f1],y] = [[[n,n1],[n,n1]],[n,n1]] &
n1 = n + 1 )
;
[f,f1] = [[n,n1],[n,n1]]
by A115, XTUPLE_0:1;
then
(
f = [n,n1] &
f1 = [n,n1] )
by XTUPLE_0:1;
hence
f |> f2
by A88;
verum end; suppose
[[f,f1],y] in { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 }
;
f |> f2then consider n,
n1 being
Element of
NAT such that A116:
(
[[f,f1],y] = [[[n,n1],n1],n1] &
n1 = n + 1 )
;
[f,f1] = [[n,n1],n1]
by A116, XTUPLE_0:1;
hence
f |> f2
by A93, XTUPLE_0:1;
verum end; suppose
[[f,f1],y] in { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) }
;
f |> f2then consider n,
n11 being
Element of
NAT such that A117:
(
[[f,f1],y] = [[n,[n,n11]],n] &
n11 = n + 1 &
n <> 0 )
;
[f,f1] = [n,[n,n11]]
by A117, XTUPLE_0:1;
then A118:
(
f = n &
f1 = [n,n11] )
by XTUPLE_0:1;
then A119:
(
n = n1 &
n11 = n2 )
by A93, XTUPLE_0:1;
[[n1,n2],n1] in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) }
by A117, A119;
then
[[f,f2],f] in the
composition of
CategoryStr(#
X,
comp #)
by A119, A118, A94, XBOOLE_0:def 3;
hence
f |> f2
by XTUPLE_0:def 12;
verum end; end;
end; hence
f |> f1 (*) f2
by A91, A88;
verum end; end; end; end;
end;
then A121:
CategoryStr(# X,comp #) is right_composable
;
for f1 being morphism of CategoryStr(# X,comp #) st f1 in the carrier of CategoryStr(# X,comp #) holds
ex f being morphism of CategoryStr(# X,comp #) st
( f |> f1 & f is left_identity )
proof
let f1 be
morphism of
CategoryStr(#
X,
comp #);
( f1 in the carrier of CategoryStr(# X,comp #) implies ex f being morphism of CategoryStr(# X,comp #) st
( f |> f1 & f is left_identity ) )
assume A122:
f1 in the
carrier of
CategoryStr(#
X,
comp #)
;
ex f being morphism of CategoryStr(# X,comp #) st
( f |> f1 & f is left_identity )
per cases
( f1 in NAT \ {0} or f1 in { [n1,n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } )
by A122, XBOOLE_0:def 3;
suppose A123:
f1 in NAT \ {0}
;
ex f being morphism of CategoryStr(# X,comp #) st
( f |> f1 & f is left_identity )then A124:
(
f1 in NAT & not
f1 in {0} )
by XBOOLE_0:def 5;
reconsider n2 =
f1 as
Element of
NAT by A123;
reconsider n22 =
n2 as
Nat ;
n22 <> 0
by A124, TARSKI:def 1;
then consider n11 being
Nat such that A125:
n22 = n11 + 1
by NAT_1:6;
reconsider n1 =
n11 as
Element of
NAT by ORDINAL1:def 12;
A126:
[n1,n2] in { [n1,n2] where n1, n2 is Element of NAT : n2 = n1 + 1 }
by A125;
then reconsider f =
[n1,n2] as
morphism of
CategoryStr(#
X,
comp #)
by XBOOLE_0:def 3;
take
f
;
( f |> f1 & f is left_identity )
[[[n1,n2],n2],n2] in { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 }
by A125;
then
[[f,f1],f1] in { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } \/ { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 }
by XBOOLE_0:def 3;
then
[[f,f1],f1] in ( { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } \/ { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ) \/ { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) }
by XBOOLE_0:def 3;
then
[[f,f1],f1] in the
composition of
CategoryStr(#
X,
comp #)
by XBOOLE_0:def 3;
hence
f |> f1
by XTUPLE_0:def 12;
f is left_identity thus
f is
left_identity
by A126, A48;
verum end; end;
end;
then A128:
CategoryStr(# X,comp #) is with_left_identities
;
for f1 being morphism of CategoryStr(# X,comp #) st f1 in the carrier of CategoryStr(# X,comp #) holds
ex f being morphism of CategoryStr(# X,comp #) st
( f1 |> f & f is right_identity )
proof
let f1 be
morphism of
CategoryStr(#
X,
comp #);
( f1 in the carrier of CategoryStr(# X,comp #) implies ex f being morphism of CategoryStr(# X,comp #) st
( f1 |> f & f is right_identity ) )
assume A129:
f1 in the
carrier of
CategoryStr(#
X,
comp #)
;
ex f being morphism of CategoryStr(# X,comp #) st
( f1 |> f & f is right_identity )
per cases
( f1 in NAT \ {0} or f1 in { [n1,n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } )
by A129, XBOOLE_0:def 3;
suppose A130:
f1 in NAT \ {0}
;
ex f being morphism of CategoryStr(# X,comp #) st
( f1 |> f & f is right_identity )then A131:
(
f1 in NAT & not
f1 in {0} )
by XBOOLE_0:def 5;
reconsider n1 =
f1 as
Element of
NAT by A130;
A132:
n1 <> 0
by A131, TARSKI:def 1;
reconsider n2 =
n1 + 1 as
Element of
NAT ;
A133:
[n1,n2] in { [n1,n2] where n1, n2 is Element of NAT : n2 = n1 + 1 }
;
then reconsider f =
[n1,n2] as
morphism of
CategoryStr(#
X,
comp #)
by XBOOLE_0:def 3;
take
f
;
( f1 |> f & f is right_identity )
[[n1,[n1,n2]],n1] in { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) }
by A132;
then
[[f1,f],f1] in ( { [[[n1,n2],[n1,n2]],[n1,n2]] where n1, n2 is Element of NAT : n2 = n1 + 1 } \/ { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ) \/ { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) }
by XBOOLE_0:def 3;
then
[[f1,f],f1] in the
composition of
CategoryStr(#
X,
comp #)
by XBOOLE_0:def 3;
hence
f1 |> f
by XTUPLE_0:def 12;
f is right_identity thus
f is
right_identity
by A133, A48;
verum end; end;
end;
then A135:
CategoryStr(# X,comp #) is with_identities
by A128, Def7;
for f1, f2, f3 being morphism of CategoryStr(# X,comp #) st f1 |> f2 & f2 |> f3 & f1 (*) f2 |> f3 & f1 |> f2 (*) f3 holds
f1 (*) (f2 (*) f3) = (f1 (*) f2) (*) f3
hence
ex b1 being CategoryStr st
( not b1 is left_composable & b1 is right_composable & b1 is with_identities & b1 is associative )
by A87, A121, A135, Def10; verum