let S1, S2 be non empty ManySortedSign ; for f, g being Function st S1,S2 are_equivalent_wrt f,g holds
S2,S1 are_equivalent_wrt f " ,g "
let f, g be Function; ( S1,S2 are_equivalent_wrt f,g implies S2,S1 are_equivalent_wrt f " ,g " )
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 S2,S1 are_equivalent_wrt f " ,g "
thus
( f " is one-to-one & g " is one-to-one )
by A1, A2; CIRCTRM1:def 9 ( f " ,g " form_morphism_between S2,S1 & (f ") " ,(g ") " form_morphism_between S1,S2 )
(f ") " = f
by A1, FUNCT_1:43;
hence
( f " ,g " form_morphism_between S2,S1 & (f ") " ,(g ") " form_morphism_between S1,S2 )
by A2, A3, A4, FUNCT_1:43; verum