let C1, C2 be non empty strict quasi-discrete AltCatStr ; :: thesis: ( the carrier of C1 = A & ( for i being object of C1 holds <^i,i^> = {(id i)} ) & the carrier of C2 = A & ( for i being object of C2 holds <^i,i^> = {(id i)} ) implies C1 = C2 )
assume that
A22: the carrier of C1 = A and
A23: for i being object of C1 holds <^i,i^> = {(id i)} and
A24: the carrier of C2 = A and
A25: for i being object of C2 holds <^i,i^> = {(id i)} ; :: thesis: C1 = C2

now

let i, j be Element of A; :: thesis: the Arrows of C1 . b₁,b₂ = the Arrows of C2 . b₁,b₂
reconsider i1 = i as object of C1 by A22;
reconsider i2 = i as object of C2 by A24;

per cases ( i = j or i <> j ) ;

suppose A26: i = j ; :: thesis: the Arrows of C1 . b₁,b₂ = the Arrows of C2 . b₁,b₂

hence the Arrows of C1 . i,j = <^i1,i1^>
.= {(id i)} by A23
.= <^i2,i2^> by A25
.= the Arrows of C2 . i,j by A26 ;
:: thesis: verum

end;

suppose A27: i <> j ; :: thesis: the Arrows of C1 . b₁,b₂ = the Arrows of C2 . b₁,b₂

reconsider j1 = j as object of C1 by A22;
reconsider j2 = j as object of C2 by A24;
thus the Arrows of C1 . i,j = <^i1,j1^>
.= {} by A27, Def20
.= <^i2,j2^> by A27, Def20
.= the Arrows of C2 . i,j ; :: thesis: verum

end;

end;

end;

then A28: the Arrows of C1 = the Arrows of C2 by A22, A24, Th9;

now

let i, j, k be set ; :: thesis: ( i in A & j in A & k in A implies the Comp of C1 . b₁,b₂,b₃ = the Comp of C2 . b₁,b₂,b₃ )
assume A29: ( i in A & j in A & k in A ) ; :: thesis: the Comp of C1 . b₁,b₂,b₃ = the Comp of C2 . b₁,b₂,b₃
then reconsider i1 = i as object of C1 by A22;
reconsider i2 = i as object of C2 by A24, A29;

per cases ( ( i = j & j = k ) or i <> j or j <> k ) ;

suppose A30: ( i = j & j = k ) ; :: thesis: the Comp of C1 . b₁,b₂,b₃ = the Comp of C2 . b₁,b₂,b₃

A31: <^i2,i2^> = {(id i2)} by A25;
A32: the Comp of C2 . i2,i2,i2 is Function of [:<^i2,i2^>,<^i2,i2^>:],<^i2,i2^> ;
A33: <^i1,i1^> = {(id i1)} by A23;
the Comp of C1 . i1,i1,i1 is Function of [:<^i1,i1^>,<^i1,i1^>:],<^i1,i1^> ;
hence the Comp of C1 . i,j,k = (id i),(id i) :-> (id i) by A30, A33, FUNCOP_1:def 10
.= the Comp of C2 . i,j,k by A30, A31, A32, FUNCOP_1:def 10 ;
:: thesis: verum

end;

suppose A34: ( i <> j or j <> k ) ; :: thesis: the Comp of C1 . b₁,b₂,b₃ = the Comp of C2 . b₁,b₂,b₃

reconsider j1 = j, k1 = k as object of C1 by A22, A29;
reconsider j2 = j, k2 = k as object of C2 by A24, A29;
( <^i2,j2^> = {} or <^j2,k2^> = {} ) by A34, Def20;
then A35: [:<^j2,k2^>,<^i2,j2^>:] = {} by ZFMISC_1:113;
A36: the Comp of C2 . i2,j2,k2 is Function of [:<^j2,k2^>,<^i2,j2^>:],<^i2,k2^> ;
( <^i1,j1^> = {} or <^j1,k1^> = {} ) by A34, Def20;
then A37: [:<^j1,k1^>,<^i1,j1^>:] = {} by ZFMISC_1:113;
the Comp of C1 . i1,j1,k1 is Function of [:<^j1,k1^>,<^i1,j1^>:],<^i1,k1^> ;
hence the Comp of C1 . i,j,k = the Comp of C2 . i,j,k by A35, A36, A37; :: thesis: verum

end;

end;

end;

hence C1 = C2 by A22, A24, A28, Th10; :: thesis: verum