let T1, T2 be Function of the carrier' of C, the carrier' of (B opp); :: thesis: ( ( for f being Morphism of C holds T1 . f = (S . f) opp ) & ( for f being Morphism of C holds T2 . f = (S . f) opp ) implies T1 = T2 )
assume that
A3: for f being Morphism of C holds T1 . f = (S . f) opp and
A4: for f being Morphism of C holds T2 . f = (S . f) opp ; :: thesis: T1 = T2

now :: thesis: for f being Morphism of C holds T1 . f = T2 . f

let f be Morphism of C; :: thesis: T1 . f = T2 . f
thus T1 . f = (S . f) opp by A3
.= T2 . f by A4 ; :: thesis: verum

end;

hence T1 = T2 by FUNCT_2:63; :: thesis: verum