let C1, C2 be non empty strict pseudo-functional AltCatStr ; :: thesis: ( the carrier of C1 = A & ( for a1, a2 being Object of C1 holds <^a1,a2^> = Funcs (a1,a2) ) & the carrier of C2 = A & ( for a1, a2 being Object of C2 holds <^a1,a2^> = Funcs (a1,a2) ) implies C1 = C2 )
assume that
A14: the carrier of C1 = A and
A15: for a1, a2 being Object of C1 holds <^a1,a2^> = Funcs (a1,a2) and
A16: the carrier of C2 = A and
A17: for a1, a2 being Object of C2 holds <^a1,a2^> = Funcs (a1,a2) ; :: thesis: C1 = C2
A18: now :: thesis: for i, j being object st i in A & j in A holds
the Arrows of C1 . (i,j) = the Arrows of C2 . (i,j)
let i, j be object ; :: thesis: ( i in A & j in A implies the Arrows of C1 . (i,j) = the Arrows of C2 . (i,j) )
assume A19: ( i in A & j in A ) ; :: thesis: the Arrows of C1 . (i,j) = the Arrows of C2 . (i,j)
then reconsider a1 = i, a2 = j as Object of C1 by A14;
reconsider b1 = i, b2 = j as Object of C2 by ;
thus the Arrows of C1 . (i,j) = <^a1,a2^>
.= Funcs (a1,a2) by A15
.= <^b1,b2^> by A17
.= the Arrows of C2 . (i,j) ; :: thesis: verum
end;
A20: 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 . (i,j,k) = the Comp of C2 . (i,j,k) )
assume A21: ( i in A & j in A & k in A ) ; :: thesis: the Comp of C1 . (i,j,k) = the Comp of C2 . (i,j,k)
then reconsider a1 = i, a2 = j, a3 = k as Object of C1 by A14;
reconsider b1 = i, b2 = j, b3 = k as Object of C2 by ;
( <^a2,a3^> = <^b2,b3^> & <^a1,a2^> = <^b1,b2^> ) by ;
hence the Comp of C1 . (i,j,k) = (FuncComp ((Funcs (b1,b2)),(Funcs (b2,b3)))) | [:<^b2,b3^>,<^b1,b2^>:] by Def13
.= the Comp of C2 . (i,j,k) by Def13 ;
:: thesis: verum
end;
the Arrows of C1 = the Arrows of C2 by A14, A16, A18, Th2;
hence C1 = C2 by A14, A16, A20, Th4; :: thesis: verum