let S1, S2 be non empty ManySortedSign ; for f, g being Function st S1,S2 are_equivalent_wrt f,g holds
( rng f = the carrier of S2 & rng g = the carrier' of S2 )
let f, g be Function; ( S1,S2 are_equivalent_wrt f,g implies ( rng f = the carrier of S2 & rng g = the carrier' of S2 ) )
assume that
A1:
f is one-to-one
and
A2:
g is one-to-one
and
f,g form_morphism_between S1,S2
and
A3:
f " ,g " form_morphism_between S2,S1
; CIRCTRM1:def 9 ( rng f = the carrier of S2 & rng g = the carrier' of S2 )
thus rng f =
dom (f ")
by A1, FUNCT_1:33
.=
the carrier of S2
by A3
; rng g = the carrier' of S2
thus rng g =
dom (g ")
by A2, FUNCT_1:33
.=
the carrier' of S2
by A3
; verum