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 ; :: thesis: ( [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 ) } ; :: thesis: ( 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 ) } ; :: thesis: 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 } ; :: thesis: y1 = y2

then 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 } ; :: thesis: y1 = y2

then 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; :: thesis: verum

end;

suppose [x,y2] in { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ; :: thesis: y1 = y2

then consider n21, n22 being Element of NAT such that
A8: ( [x,y2] = [[[n21,n22],n22],n22] & n22 = n21 + 1 ) ;
( x = [[n21,n22],n22] & y2 = n22 ) by A8, XTUPLE_0:1;
hence y1 = y2 by A6, XTUPLE_0:1; :: thesis: verum

end;

suppose [x,y2] in { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } ; :: thesis: y1 = y2

then consider n21, n22 being Element of NAT such that
A9: ( [x,y2] = [[n21,[n21,n22]],n21] & n22 = n21 + 1 & n21 <> 0 ) ;
( x = [n21,[n21,n22]] & y2 = n21 ) by A9, XTUPLE_0:1;
hence y1 = y2 by A6, XTUPLE_0:1; :: thesis: verum

end;

suppose [x,y2] in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } ; :: thesis: y1 = y2

then consider n21, n22 being Element of NAT such that
A10: ( [x,y2] = [[n21,n22],n21] & n22 = n21 + 1 & n21 <> 0 ) ;
( x = [n21,n22] & y2 = n21 ) by A10, XTUPLE_0:1;
hence y1 = y2 by A6, XTUPLE_0:1; :: thesis: verum

end;

end;

end;

suppose [x,y1] in { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ; :: thesis: y1 = y2

then 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 } ; :: thesis: y1 = y2

then 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; :: thesis: verum

end;

suppose [x,y2] in { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ; :: thesis: y1 = y2

then consider n21, n22 being Element of NAT such that
A14: ( [x,y2] = [[[n21,n22],n22],n22] & n22 = n21 + 1 ) ;
( x = [[n21,n22],n22] & y2 = n22 ) by A14, XTUPLE_0:1;
hence y1 = y2 by A12, XTUPLE_0:1; :: thesis: verum

end;

suppose [x,y2] in { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } ; :: thesis: y1 = y2

then consider n21, n22 being Element of NAT such that
A15: ( [x,y2] = [[n21,[n21,n22]],n21] & n22 = n21 + 1 & n21 <> 0 ) ;
( x = [n21,[n21,n22]] & y2 = n21 ) by A15, XTUPLE_0:1;
hence y1 = y2 by A12, XTUPLE_0:1; :: thesis: verum

end;

suppose [x,y2] in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } ; :: thesis: y1 = y2

then consider n21, n22 being Element of NAT such that
A16: ( [x,y2] = [[n21,n22],n21] & n22 = n21 + 1 & n21 <> 0 ) ;
( x = [n21,n22] & y2 = n21 ) by A16, XTUPLE_0:1;
hence y1 = y2 by A12, XTUPLE_0:1; :: thesis: verum

end;

end;

end;

suppose [x,y1] in { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } ; :: thesis: y1 = y2

then 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 } ; :: thesis: y1 = y2

then 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; :: thesis: verum

end;

suppose [x,y2] in { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ; :: thesis: y1 = y2

then consider n21, n22 being Element of NAT such that
A20: ( [x,y2] = [[[n21,n22],n22],n22] & n22 = n21 + 1 ) ;
( x = [[n21,n22],n22] & y2 = n22 ) by A20, XTUPLE_0:1;
hence y1 = y2 by A18, XTUPLE_0:1; :: thesis: verum

end;

suppose [x,y2] in { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } ; :: thesis: y1 = y2

then consider n21, n22 being Element of NAT such that
A21: ( [x,y2] = [[n21,[n21,n22]],n21] & n22 = n21 + 1 & n21 <> 0 ) ;
( x = [n21,[n21,n22]] & y2 = n21 ) by A21, XTUPLE_0:1;
hence y1 = y2 by A18, XTUPLE_0:1; :: thesis: verum

end;

suppose [x,y2] in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } ; :: thesis: y1 = y2

then consider n21, n22 being Element of NAT such that
A22: ( [x,y2] = [[n21,n22],n21] & n22 = n21 + 1 & n21 <> 0 ) ;
( x = [n21,n22] & y2 = n21 ) by A22, XTUPLE_0:1;
hence y1 = y2 by A18, XTUPLE_0:1; :: thesis: verum

end;

end;

end;

suppose [x,y1] in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } ; :: thesis: y1 = y2

then 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 } ; :: thesis: y1 = y2

then 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; :: thesis: verum

end;

suppose [x,y2] in { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ; :: thesis: y1 = y2

then consider n21, n22 being Element of NAT such that
A26: ( [x,y2] = [[[n21,n22],n22],n22] & n22 = n21 + 1 ) ;
( x = [[n21,n22],n22] & y2 = n22 ) by A26, XTUPLE_0:1;
hence y1 = y2 by A24, XTUPLE_0:1; :: thesis: verum

end;

suppose [x,y2] in { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } ; :: thesis: y1 = y2

then consider n21, n22 being Element of NAT such that
A27: ( [x,y2] = [[n21,[n21,n22]],n21] & n22 = n21 + 1 & n21 <> 0 ) ;
( x = [n21,[n21,n22]] & y2 = n21 ) by A27, XTUPLE_0:1;
hence y1 = y2 by A24, XTUPLE_0:1; :: thesis: verum

end;

suppose [x,y2] in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } ; :: thesis: y1 = y2

then consider n21, n22 being Element of NAT such that
A28: ( [x,y2] = [[n21,n22],n21] & n22 = n21 + 1 & n21 <> 0 ) ;
( x = [n21,n22] & y2 = n21 ) by A28, XTUPLE_0:1;
hence y1 = y2 by A24, XTUPLE_0:1; :: thesis: 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 ; :: thesis: ( 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 ) } ; :: thesis: 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 } ; :: thesis: 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; :: thesis: verum

end;

suppose x in { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ; :: thesis: 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; :: thesis: verum

end;

suppose x in { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } ; :: thesis: 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; :: thesis: verum

end;

suppose x in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } ; :: thesis: 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; :: thesis: 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 #)

proof

let n1 be Element of NAT ; :: thesis: ( n1 <> 0 implies n1 is morphism of CategoryStr(# X,comp #) )
assume n1 <> 0 ; :: thesis: n1 is morphism of CategoryStr(# X,comp #)
then not n1 in {0} by TARSKI:def 1;
then n1 in NAT \ {0} by XBOOLE_0:def 5;
hence n1 is morphism of CategoryStr(# X,comp #) by XBOOLE_0:def 3; :: thesis: verum

end;

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 #); :: thesis: 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 ; :: thesis: ( f1 = n1 & f2 = n2 & n2 = n1 + 1 & n1 <> 0 implies ( f1 |> f2 & f1 (*) f2 = f1 ) )
assume A43: ( f1 = n1 & f2 = n2 ) ; :: thesis: ( not n2 = n1 + 1 or not n1 <> 0 or ( f1 |> f2 & f1 (*) f2 = f1 ) )
assume ( n2 = n1 + 1 & n1 <> 0 ) ; :: thesis: ( 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; :: thesis: 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 ; :: thesis: 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 #); :: thesis: ( 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 } ; :: thesis: ( 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 #); :: thesis: ( f |> f1 implies f (*) f1 = f1 )
assume A50: f |> f1 ; :: thesis: 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 } ; :: thesis: f (*) f1 = f1

then 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 ; :: thesis: verum

end;

suppose [[f,f1],y] in { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ; :: thesis: f (*) f1 = f1

then 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 ; :: thesis: verum

end;

suppose [[f,f1],y] in { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } ; :: thesis: f (*) f1 = f1

then 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; :: thesis: verum

end;

suppose [[f,f1],y] in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } ; :: thesis: f (*) f1 = f1

then consider n1, n2 being Element of NAT such that
A58: ( [[f,f1],y] = [[n1,n2],n1] & n2 = n1 + 1 & n1 <> 0 ) ;
[f,f1] = [n1,n2] by A58, XTUPLE_0:1;
hence f (*) f1 = f1 by A49, XTUPLE_0:1; :: thesis: verum

end;

end;

end;

hence f is left_identity ; :: thesis: ( 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 #); :: thesis: ( f1 |> f implies f1 (*) f = f1 )
assume A59: f1 |> f ; :: thesis: 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 } ; :: thesis: f1 (*) f = f1

then 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 ; :: thesis: verum

end;

suppose [[f1,f],y] in { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ; :: thesis: f1 (*) f = f1

then 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; :: thesis: verum

end;

suppose [[f1,f],y] in { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } ; :: thesis: f1 (*) f = f1

then 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 ; :: thesis: verum

end;

suppose [[f1,f],y] in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } ; :: thesis: f1 (*) f = f1

then consider n1, n2 being Element of NAT such that
A67: ( [[f1,f],y] = [[n1,n2],n1] & n2 = n1 + 1 & n1 <> 0 ) ;
[f1,f] = [n1,n2] by A67, XTUPLE_0:1;
hence f1 (*) f = f1 by A49, XTUPLE_0:1; :: thesis: verum

end;

end;

end;

hence f is right_identity ; :: thesis: 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; :: thesis: 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 #); :: thesis: ( f1 in NAT \ {0} & f1 |> f2 implies f1 (*) f2 = f1 )
assume A69: f1 in NAT \ {0} ; :: thesis: ( not f1 |> f2 or f1 (*) f2 = f1 )
reconsider nf1 = f1 as Element of NAT by A69;
assume A70: f1 |> f2 ; :: thesis: 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} ; :: thesis: f1 (*) f2 = f1

reconsider 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 } ; :: thesis: f1 (*) f2 = f1

then 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; :: thesis: verum

end;

suppose [[f1,f2],y] in { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ; :: thesis: f1 (*) f2 = f1

then 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; :: thesis: verum

end;

suppose [[f1,f2],y] in { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } ; :: thesis: f1 (*) f2 = f1

then 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; :: thesis: verum

end;

suppose [[f1,f2],y] in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } ; :: thesis: f1 (*) f2 = f1

then 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 ; :: thesis: verum

end;

end;

end;

suppose f2 in { [n1,n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ; :: thesis: f1 (*) f2 = f1

then f2 is right_identity by A48;
hence f1 (*) f2 = f1 by A70; :: thesis: verum

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 ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: ( f1 |> f2 & ( ( f1 (*) f2 |> f & not f2 |> f ) or ( f2 |> f & not f1 (*) f2 |> f ) ) )
A79: 2 = 1 + 1 ;
hence f1 |> f2 by A42; :: thesis: ( ( f1 (*) f2 |> f & not f2 |> f ) or ( f2 |> f & not f1 (*) f2 |> f ) )
A80: not f1 |> f

proof

assume f1 |> f ; :: thesis: 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 } ; :: thesis: contradiction

then 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; :: thesis: verum

end;

suppose [[f1,f],y] in { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ; :: thesis: contradiction

then 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; :: thesis: verum

end;

suppose [[f1,f],y] in { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } ; :: thesis: contradiction

then 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; :: thesis: verum

end;

suppose [[f1,f],y] in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } ; :: thesis: contradiction

then consider n1, n2 being Element of NAT such that
A86: ( [[f1,f],y] = [[n1,n2],n1] & n2 = n1 + 1 & n1 <> 0 ) ;
[f1,f] = [n1,n2] by A86, XTUPLE_0:1;
then ( f1 = n1 & f = n2 ) by XTUPLE_0:1;
hence contradiction by A86; :: thesis: 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; :: thesis: 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 #); :: thesis: ( f1 |> f2 implies ( f |> f1 (*) f2 iff f |> f1 ) )
assume A88: f1 |> f2 ; :: thesis: ( 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} ; :: thesis: ( 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 f1 in NAT \ {0} ; :: thesis: ( f |> f1 (*) f2 iff f |> f1 )

hence ( f |> f1 (*) f2 iff f |> f1 ) by A88, A68; :: thesis: verum

end;

suppose A90: f1 in { [n1,n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ; :: thesis: ( 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 ; :: thesis: 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 } ; :: thesis: contradiction

then 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; :: thesis: verum

end;

suppose [[f1,f2],y] in { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ; :: thesis: contradiction

then 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; :: thesis: verum

end;

suppose [[f1,f2],y] in { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } ; :: thesis: contradiction

then 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; :: thesis: verum

end;

suppose [[f1,f2],y] in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } ; :: thesis: contradiction

then consider n1, n2 being Element of NAT such that
A101: ( [[f1,f2],y] = [[n1,n2],n1] & n2 = n1 + 1 & n1 <> 0 ) ;
[f1,f2] = [n1,n2] by A101, XTUPLE_0:1;
hence contradiction by A93, XTUPLE_0:1; :: thesis: verum

end;

end;

end;

hereby :: thesis: ( f |> f1 implies f |> f1 (*) f2 )

assume f |> f1 (*) f2 ; :: thesis: f |> f1
then 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 } ; :: thesis: f |> f1

then 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; :: thesis: verum

end;

suppose [[f,f2],y] in { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ; :: thesis: f |> f1

then 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; :: thesis: verum

end;

suppose [[f,f2],y] in { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } ; :: thesis: f |> f1

then 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; :: thesis: verum

end;

suppose [[f,f2],y] in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } ; :: thesis: f |> f1

then 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; :: thesis: verum

end;

end;

end;

assume A112: f |> f1 ; :: thesis: 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 } ; :: thesis: f |> f2

then 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; :: thesis: verum

end;

suppose [[f,f1],y] in { [[[n1,n2],n2],n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ; :: thesis: f |> f2

then 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; :: thesis: verum

end;

suppose [[f,f1],y] in { [[n1,[n1,n2]],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } ; :: thesis: f |> f2

then 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; :: thesis: verum

end;

suppose [[f,f1],y] in { [[n1,n2],n1] where n1, n2 is Element of NAT : ( n2 = n1 + 1 & n1 <> 0 ) } ; :: thesis: f |> f2

then consider n, n1 being Element of NAT such that
A120: ( [[f,f1],y] = [[n,n1],n] & n1 = n + 1 & n <> 0 ) ;
[f,f1] = [n,n1] by A120, XTUPLE_0:1;
hence f |> f2 by A93, XTUPLE_0:1; :: thesis: verum

end;

end;

end;

hence f |> f1 (*) f2 by A91, A88; :: thesis: verum

end;

end;

end;

suppose f2 in { [n1,n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ; :: thesis: ( f |> f1 (*) f2 iff f |> f1 )

then f2 is right_identity by A48;
hence ( f |> f1 (*) f2 iff f |> f1 ) by A88; :: thesis: verum

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 #); :: thesis: ( 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 #) ; :: thesis: 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} ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: f is left_identity
thus f is left_identity by A126, A48; :: thesis: verum

end;

suppose A127: f1 in { [n1,n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ; :: thesis: ex f being morphism of CategoryStr(# X,comp #) st
( f |> f1 & f is left_identity )

set f = f1;
take f1 ; :: thesis: ( f1 |> f1 & f1 is left_identity )
thus ( f1 |> f1 & f1 is left_identity ) by A127, A48; :: thesis: 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 #); :: thesis: ( 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 #) ; :: thesis: 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} ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: f is right_identity
thus f is right_identity by A133, A48; :: thesis: verum

end;

suppose A134: f1 in { [n1,n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ; :: thesis: ex f being morphism of CategoryStr(# X,comp #) st
( f1 |> f & f is right_identity )

set f = f1;
take f1 ; :: thesis: ( f1 |> f1 & f1 is right_identity )
thus ( f1 |> f1 & f1 is right_identity ) by A134, A48; :: thesis: 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

proof

let f1, f2, f3 be morphism of CategoryStr(# X,comp #); :: thesis: ( f1 |> f2 & f2 |> f3 & f1 (*) f2 |> f3 & f1 |> f2 (*) f3 implies f1 (*) (f2 (*) f3) = (f1 (*) f2) (*) f3 )
assume A136: f1 |> f2 ; :: thesis: ( not f2 |> f3 or not f1 (*) f2 |> f3 or not f1 |> f2 (*) f3 or f1 (*) (f2 (*) f3) = (f1 (*) f2) (*) f3 )
assume f2 |> f3 ; :: thesis: ( not f1 (*) f2 |> f3 or not f1 |> f2 (*) f3 or f1 (*) (f2 (*) f3) = (f1 (*) f2) (*) f3 )
assume A137: f1 (*) f2 |> f3 ; :: thesis: ( not f1 |> f2 (*) f3 or f1 (*) (f2 (*) f3) = (f1 (*) f2) (*) f3 )
assume A138: f1 |> f2 (*) f3 ; :: thesis: f1 (*) (f2 (*) f3) = (f1 (*) f2) (*) f3
A139: not CategoryStr(# X,comp #) is empty by A136;

per cases ( f1 in NAT \ {0} or f1 in { [n1,n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ) by A139, XBOOLE_0:def 3;

suppose A140: f1 in NAT \ {0} ; :: thesis: f1 (*) (f2 (*) f3) = (f1 (*) f2) (*) f3

then A141: ( f1 (*) (f2 (*) f3) = f1 & f1 (*) f2 = f1 ) by A136, A138, A68;
thus f1 (*) (f2 (*) f3) = (f1 (*) f2) (*) f3 by A140, A68, A141, A137; :: thesis: verum

end;

suppose f1 in { [n1,n2] where n1, n2 is Element of NAT : n2 = n1 + 1 } ; :: thesis: f1 (*) (f2 (*) f3) = (f1 (*) f2) (*) f3

then f1 is left_identity by A48;
then ( f1 (*) (f2 (*) f3) = f2 (*) f3 & f1 (*) f2 = f2 ) by A136, A138;
hence f1 (*) (f2 (*) f3) = (f1 (*) f2) (*) f3 ; :: thesis: verum

end;

end;

end;

hence ex b₁ being CategoryStr st
( not b₁ is left_composable & b₁ is right_composable & b₁ is with_identities & b₁ is associative ) by A87, A121, A135, Def10; :: thesis: verum