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

hence C1 = C2 by A14, A16, A20, Th4; :: thesis: verum

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)

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 A16, A19;

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;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 A16, A19;

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

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)

the Arrows of C1 = the Arrows of C2
by A14, A16, A18, Th2;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 A16, A21;

( <^a2,a3^> = <^b2,b3^> & <^a1,a2^> = <^b1,b2^> ) by A14, A18;

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;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 A16, A21;

( <^a2,a3^> = <^b2,b3^> & <^a1,a2^> = <^b1,b2^> ) by A14, A18;

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

hence C1 = C2 by A14, A16, A20, Th4; :: thesis: verum