let S1, S2 be non empty ManySortedSign ; :: thesis: 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; :: thesis: ( 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 ; :: according to CIRCTRM1:def 9 :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: verum