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

assume that

A1: for f being Morphism of (C opp) holds T1 . f = S . (opp f) and

A2: for f being Morphism of (C opp) holds T2 . f = S . (opp f) ; :: thesis: T1 = T2

assume that

A1: for f being Morphism of (C opp) holds T1 . f = S . (opp f) and

A2: for f being Morphism of (C opp) holds T2 . f = S . (opp f) ; :: thesis: T1 = T2

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

hence
T1 = T2
by FUNCT_2:63; :: thesis: verumlet f be Morphism of (C opp); :: thesis: T1 . f = T2 . f

thus T1 . f = S . (opp f) by A1

.= T2 . f by A2 ; :: thesis: verum

end;thus T1 . f = S . (opp f) by A1

.= T2 . f by A2 ; :: thesis: verum