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

A20: the carrier of C1 = A and

A21: for i being Object of C1 holds <^i,i^> = {(id i)} and

A22: the carrier of C2 = A and

A23: for i being Object of C2 holds <^i,i^> = {(id i)} ; :: thesis: C1 = C2

hence C1 = C2 by A20, A22, A24, Th4; :: thesis: verum

assume that

A20: the carrier of C1 = A and

A21: for i being Object of C1 holds <^i,i^> = {(id i)} and

A22: the carrier of C2 = A and

A23: for i being Object of C2 holds <^i,i^> = {(id i)} ; :: thesis: C1 = C2

A24: now :: thesis: for i, j, k being object st i in A & j in A & k in A holds

the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k)

the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k)

let i, j, k be object ; :: thesis: ( i in A & j in A & k in A implies the Comp of C1 . (b_{1},b_{2},b_{3}) = the Comp of C2 . (b_{1},b_{2},b_{3}) )

assume that

A25: i in A and

A26: ( j in A & k in A ) ; :: thesis: the Comp of C1 . (b_{1},b_{2},b_{3}) = the Comp of C2 . (b_{1},b_{2},b_{3})

reconsider i2 = i as Object of C2 by A22, A25;

reconsider i1 = i as Object of C1 by A20, A25;

end;assume that

A25: i in A and

A26: ( j in A & k in A ) ; :: thesis: the Comp of C1 . (b

reconsider i2 = i as Object of C2 by A22, A25;

reconsider i1 = i as Object of C1 by A20, A25;

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

end;

suppose A27:
( i = j & j = k )
; :: thesis: the Comp of C1 . (b_{1},b_{2},b_{3}) = the Comp of C2 . (b_{1},b_{2},b_{3})

A28:
( <^i2,i2^> = {(id i2)} & the Comp of C2 . (i2,i2,i2) is Function of [:<^i2,i2^>,<^i2,i2^>:],<^i2,i2^> )
by A23;

reconsider ii = i as set by TARSKI:1;

( <^i1,i1^> = {(id i1)} & the Comp of C1 . (i1,i1,i1) is Function of [:<^i1,i1^>,<^i1,i1^>:],<^i1,i1^> ) by A21;

hence the Comp of C1 . (i,j,k) = ((id ii),(id ii)) :-> (id ii) by A27, FUNCOP_1:def 10

.= the Comp of C2 . (i,j,k) by A27, A28, FUNCOP_1:def 10 ;

:: thesis: verum

end;reconsider ii = i as set by TARSKI:1;

( <^i1,i1^> = {(id i1)} & the Comp of C1 . (i1,i1,i1) is Function of [:<^i1,i1^>,<^i1,i1^>:],<^i1,i1^> ) by A21;

hence the Comp of C1 . (i,j,k) = ((id ii),(id ii)) :-> (id ii) by A27, FUNCOP_1:def 10

.= the Comp of C2 . (i,j,k) by A27, A28, FUNCOP_1:def 10 ;

:: thesis: verum

suppose A29:
( i <> j or j <> k )
; :: thesis: the Comp of C1 . (b_{1},b_{2},b_{3}) = the Comp of C2 . (b_{1},b_{2},b_{3})

reconsider j1 = j, k1 = k as Object of C1 by A20, A26;

A30: ( <^i1,j1^> = {} or <^j1,k1^> = {} ) by A29, Def18;

reconsider j2 = j, k2 = k as Object of C2 by A22, A26;

A31: ( the Comp of C2 . (i2,j2,k2) is Function of [:<^j2,k2^>,<^i2,j2^>:],<^i2,k2^> & the Comp of C1 . (i1,j1,k1) is Function of [:<^j1,k1^>,<^i1,j1^>:],<^i1,k1^> ) ;

( <^i2,j2^> = {} or <^j2,k2^> = {} ) by A29, Def18;

hence the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k) by A30, A31; :: thesis: verum

end;A30: ( <^i1,j1^> = {} or <^j1,k1^> = {} ) by A29, Def18;

reconsider j2 = j, k2 = k as Object of C2 by A22, A26;

A31: ( the Comp of C2 . (i2,j2,k2) is Function of [:<^j2,k2^>,<^i2,j2^>:],<^i2,k2^> & the Comp of C1 . (i1,j1,k1) is Function of [:<^j1,k1^>,<^i1,j1^>:],<^i1,k1^> ) ;

( <^i2,j2^> = {} or <^j2,k2^> = {} ) by A29, Def18;

hence the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k) by A30, A31; :: thesis: verum

now :: thesis: for i, j being Element of A holds the Arrows of C1 . (i,j) = the Arrows of C2 . (i,j)

then
the Arrows of C1 = the Arrows of C2
by A20, A22, Th3;let i, j be Element of A; :: thesis: the Arrows of C1 . (b_{1},b_{2}) = the Arrows of C2 . (b_{1},b_{2})

reconsider i2 = i as Object of C2 by A22;

reconsider i1 = i as Object of C1 by A20;

end;reconsider i2 = i as Object of C2 by A22;

reconsider i1 = i as Object of C1 by A20;

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

end;

suppose A32:
i = j
; :: thesis: the Arrows of C1 . (b_{1},b_{2}) = the Arrows of C2 . (b_{1},b_{2})

hence the Arrows of C1 . (i,j) =
<^i1,i1^>

.= {(id i)} by A21

.= <^i2,i2^> by A23

.= the Arrows of C2 . (i,j) by A32 ;

:: thesis: verum

end;.= {(id i)} by A21

.= <^i2,i2^> by A23

.= the Arrows of C2 . (i,j) by A32 ;

:: thesis: verum

suppose A33:
i <> j
; :: thesis: the Arrows of C1 . (b_{1},b_{2}) = the Arrows of C2 . (b_{1},b_{2})

reconsider j2 = j as Object of C2 by A22;

reconsider j1 = j as Object of C1 by A20;

thus the Arrows of C1 . (i,j) = <^i1,j1^>

.= {} by A33, Def18

.= <^i2,j2^> by A33, Def18

.= the Arrows of C2 . (i,j) ; :: thesis: verum

end;reconsider j1 = j as Object of C1 by A20;

thus the Arrows of C1 . (i,j) = <^i1,j1^>

.= {} by A33, Def18

.= <^i2,j2^> by A33, Def18

.= the Arrows of C2 . (i,j) ; :: thesis: verum

hence C1 = C2 by A20, A22, A24, Th4; :: thesis: verum