reconsider X = {0,1} as set ;
set comp = {[[0,0],0],[[0,1],1]};
A1: for x, y1, y2 being object st [x,y1] in {[[0,0],0],[[0,1],1]} & [x,y2] in {[[0,0],0],[[0,1],1]} holds
y1 = y2

proof

let x, y1, y2 be object ; :: thesis:
assume A2: [x,y1] in {[[0,0],0],[[0,1],1]} ; :: thesis:
assume A3: [x,y2] in {[[0,0],0],[[0,1],1]} ; :: thesis:

per cases = [[0,0],0] or [x,y1] = [[0,1],1] ) by A2, TARSKI:def 2;

suppose A4: [x,y1] = [[0,0],0] ; :: thesis:

then A5: ( x = [0,0] & y1 = 0 ) by XTUPLE_0:1;

per cases = [[0,0],0] or [x,y2] = [[0,1],1] ) by A3, TARSKI:def 2;

suppose [x,y2] = [[0,0],0] ; :: thesis:

hence y1 = y2 by A4, XTUPLE_0:1; :: thesis:

end;

suppose [x,y2] = [[0,1],1] ; :: thesis:

then ( x = [0,1] & y2 = 1 ) by XTUPLE_0:1;
hence y1 = y2 by A5, XTUPLE_0:1; :: thesis:

end;

end;

end;

suppose A6: [x,y1] = [[0,1],1] ; :: thesis:

then A7: ( x = [0,1] & y1 = 1 ) by XTUPLE_0:1;

per cases = [[0,0],0] or [x,y2] = [[0,1],1] ) by A3, TARSKI:def 2;

suppose [x,y2] = [[0,0],0] ; :: thesis:

then ( x = [0,0] & y2 = 0 ) by XTUPLE_0:1;
hence y1 = y2 by A7, XTUPLE_0:1; :: thesis:

end;

suppose [x,y2] = [[0,1],1] ; :: thesis:

hence y1 = y2 by A6, XTUPLE_0:1; :: thesis:

end;

end;

end;

end;

end;

for x being object st x in {[[0,0],0],[[0,1],1]} holds
x in [:[:X,X:],X:]

proof

let x be object ; :: thesis:
assume A8: x in {[[0,0],0],[[0,1],1]} ; :: thesis:

per cases by A8, TARSKI:def 2;

suppose A9: x = [[0,0],0] ; :: thesis:

A10: 0 in X by TARSKI:def 2;
then [0,0] in [:X,X:] by ZFMISC_1:def 2;
hence x in [:[:X,X:],X:] by A9, A10, ZFMISC_1:def 2; :: thesis:

end;

suppose A11: x = [[0,1],1] ; :: thesis:

A12: ( 0 in X & 1 in X ) by TARSKI:def 2;
then [0,1] in [:X,X:] by ZFMISC_1:def 2;
hence x in [:[:X,X:],X:] by A11, A12, ZFMISC_1:def 2; :: thesis:

end;

end;

end;

then reconsider comp = {[[0,0],0],[[0,1],1]} as PartFunc of [:X,X:],X by A1, TARSKI:def 3, FUNCT_1:def 1;
set C = CategoryStr(# X,comp #);
A13: for f1, f2 being morphism of CategoryStr(# X,comp #) holds
( not f1 |> f2 or ( f1 = 0 & f2 = 0 & f1 (*) f2 = 0 ) or ( f1 = 0 & f2 = 1 & f1 (*) f2 = 1 ) )

proof

let f1, f2 be morphism of CategoryStr(# X,comp #); :: thesis:
assume A14: f1 |> f2 ; :: thesis:
assume A15: ( not f1 = 0 or not f2 = 0 or not f1 (*) f2 = 0 ) ; :: thesis:
consider y being object such that
A16: [[f1,f2],y] in the composition of CategoryStr(# X,comp #) by A14, XTUPLE_0:def 12;
A17: f1 (*) f2 = the composition of CategoryStr(# X,comp #) . (f1,f2) by Def3, A14
.= the composition of CategoryStr(# X,comp #) . [f1,f2] by BINOP_1:def 1
.= y by A16, FUNCT_1:1 ;

per cases = [[0,0],0] or [[f1,f2],y] = [[0,1],1] ) by A16, TARSKI:def 2;

suppose [[f1,f2],y] = [[0,0],0] ; :: thesis:

then ( [f1,f2] = [0,0] & y = 0 ) by XTUPLE_0:1;
hence ( f1 = 0 & f2 = 1 & f1 (*) f2 = 1 ) by A17, A15, XTUPLE_0:1; :: thesis:

end;

suppose [[f1,f2],y] = [[0,1],1] ; :: thesis:

then ( [f1,f2] = [0,1] & y = 1 ) by XTUPLE_0:1;
hence ( f1 = 0 & f2 = 1 & f1 (*) f2 = 1 ) by A17, XTUPLE_0:1; :: thesis:

end;

end;

end;

A18: for f1, f2 being morphism of CategoryStr(# X,comp #) st f1 |> f2 holds
( f1 = 0 & ( f2 = 0 or f2 = 1 ) )

proof

let f1, f2 be morphism of CategoryStr(# X,comp #); :: thesis:
assume f1 |> f2 ; :: thesis:
then consider y being object such that
A19: [[f1,f2],y] in the composition of CategoryStr(# X,comp #) by XTUPLE_0:def 12;

per cases = [[0,0],0] or [[f1,f2],y] = [[0,1],1] ) by A19, TARSKI:def 2;

suppose [[f1,f2],y] = [[0,0],0] ; :: thesis:

then ( [f1,f2] = [0,0] & y = 0 ) by XTUPLE_0:1;
hence ( f1 = 0 & ( f2 = 0 or f2 = 1 ) ) by XTUPLE_0:1; :: thesis:

end;

suppose [[f1,f2],y] = [[0,1],1] ; :: thesis:

then ( [f1,f2] = [0,1] & y = 1 ) by XTUPLE_0:1;
hence ( f1 = 0 & ( f2 = 0 or f2 = 1 ) ) by XTUPLE_0:1; :: thesis:

end;

end;

end;

A20: for f1, f2 being morphism of CategoryStr(# X,comp #) st f1 = 0 holds
f1 |> f2

proof

let f1, f2 be morphism of CategoryStr(# X,comp #); :: thesis:
assume A21: f1 = 0 ; :: thesis:
( f2 = 0 or f2 = 1 ) by TARSKI:def 2;
then [[f1,f2],f2] in the composition of CategoryStr(# X,comp #) by A21, TARSKI:def 2;
hence f1 |> f2 by FUNCT_1:1; :: thesis:

end;

for f, f1, f2 being morphism of CategoryStr(# X,comp #) st f1 |> f2 holds
( f1 (*) f2 |> f iff f2 |> f )

proof

let f, f1, f2 be morphism of CategoryStr(# X,comp #); :: thesis:
assume A22: f1 |> f2 ; :: thesis:

per cases by A22, A13;

suppose ( f1 = 0 & f2 = 0 & f1 (*) f2 = 0 ) ; :: thesis:

hence ( f1 (*) f2 |> f iff f2 |> f ) ; :: thesis:

end;

suppose ( f1 = 0 & f2 = 1 & f1 (*) f2 = 1 ) ; :: thesis:

hence ( f1 (*) f2 |> f iff f2 |> f ) ; :: thesis:

end;

end;

end;

then A23: 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:
assume A24: f1 |> f2 ; :: thesis:

per cases by A24, A13;

suppose ( f1 = 0 & f2 = 0 & f1 (*) f2 = 0 ) ; :: thesis:

hence ( f |> f1 (*) f2 iff f |> f1 ) ; :: thesis:

end;

suppose ( f1 = 0 & f2 = 1 & f1 (*) f2 = 1 ) ; :: thesis:

hereby :: thesis:

assume f |> f1 (*) f2 ; :: thesis:
then f = 0 by A18;
hence f |> f1 by A20; :: thesis:

end;

assume f |> f1 ; :: thesis:
then f = 0 by A18;
hence f |> f1 (*) f2 by A20; :: thesis:

end;

end;

end;

then A25: CategoryStr(# X,comp #) is composable by A23, Def9;
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:
assume f1 in the carrier of CategoryStr(# X,comp #) ; :: thesis:
reconsider f = 0 as morphism of CategoryStr(# X,comp #) by TARSKI:def 2;
take f ; :: thesis:
thus f |> f1 by A20; :: thesis:
for f2 being morphism of CategoryStr(# X,comp #) st f |> f2 holds
f (*) f2 = f2

proof

let f2 be morphism of CategoryStr(# X,comp #); :: thesis:
assume A26: f |> f2 ; :: thesis:
( f2 = 0 or f2 = 1 ) by TARSKI:def 2;
hence f (*) f2 = f2 by A26, A13; :: thesis:

end;

hence f is left_identity ; :: thesis:

end;

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

proof

reconsider f1 = 1 as morphism of CategoryStr(# X,comp #) by TARSKI:def 2;
take f1 ; :: thesis:
thus f1 in the carrier of CategoryStr(# X,comp #) ; :: thesis:
let f be morphism of CategoryStr(# X,comp #); :: thesis:
assume f1 |> f ; :: thesis:
hence not f is right_identity by A18; :: thesis:

end;

then A28: not CategoryStr(# X,comp #) is with_right_identities ;
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:
assume A29: ( f1 |> f2 & f2 |> f3 ) ; :: thesis:
assume A30: f1 (*) f2 |> f3 ; :: thesis:
assume A31: f1 |> f2 (*) f3 ; :: thesis:

per cases by TARSKI:def 2;

suppose A32: f3 = 0 ; :: thesis:

then f2 (*) f3 = 0 by A29, A13;
hence f1 (*) (f2 (*) f3) = 0 by A31, A13
.= (f1 (*) f2) (*) f3 by A30, A32, A13 ;
:: thesis:

end;

suppose A33: f3 = 1 ; :: thesis:

then f2 (*) f3 = 1 by A29, A13;
hence f1 (*) (f2 (*) f3) = 1 by A31, A13
.= (f1 (*) f2) (*) f3 by A30, A33, A13 ;
:: thesis:

end;

end;

end;

hence ex b₁ being CategoryStr st
( b₁ is with_left_identities & not b₁ is with_right_identities & b₁ is composable & b₁ is associative ) by A25, A27, A28, Def10; :: thesis: