let S1, S2 be non empty ManySortedSign ; :: thesis: 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; :: thesis: ( 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 & g is one-to-one ) and
f,g form_morphism_between S1,S2 and
A2: f " ,g " form_morphism_between S2,S1 ; :: according to CIRCTRM1:def 9 :: thesis: ( rng f = the carrier of S2 & rng g = the carrier' of S2 )
thus rng f = dom (f " ) by A1, FUNCT_1:55
.= the carrier of S2 by A2, PUA2MSS1:def 13 ; :: thesis: rng g = the carrier' of S2
thus rng g = dom (g " ) by A1, FUNCT_1:55
.= the carrier' of S2 by A2, PUA2MSS1:def 13 ; :: thesis: verum