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
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)
let i, j, k be object ; :: thesis: ( i in A & j in A & k in A implies the Comp of C1 . (b1,b2,b3) = the Comp of C2 . (b1,b2,b3) )
assume that
A25: i in A and
A26: ( j in A & k in A ) ; :: thesis: the Comp of C1 . (b1,b2,b3) = the Comp of C2 . (b1,b2,b3)
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 ) ;
suppose A27: ( i = j & j = k ) ; :: thesis: the Comp of C1 . (b1,b2,b3) = the Comp of C2 . (b1,b2,b3)
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;
suppose A29: ( i <> j or j <> k ) ; :: thesis: the Comp of C1 . (b1,b2,b3) = the Comp of C2 . (b1,b2,b3)
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;
end;
end;
now :: thesis: for i, j being Element of A holds the Arrows of C1 . (i,j) = the Arrows of C2 . (i,j)
let i, j be Element of A; :: thesis: the Arrows of C1 . (b1,b2) = the Arrows of C2 . (b1,b2)
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 ) ;
suppose A32: i = j ; :: thesis: the Arrows of C1 . (b1,b2) = the Arrows of C2 . (b1,b2)
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;
suppose A33: i <> j ; :: thesis: the Arrows of C1 . (b1,b2) = the Arrows of C2 . (b1,b2)
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;
end;
end;
then the Arrows of C1 = the Arrows of C2 by A20, A22, Th3;
hence C1 = C2 by A20, A22, A24, Th4; :: thesis: verum