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