let S1, S2 be non empty ManySortedSign ; :: thesis: ( ex f, g being one-to-one Function st S1,S2 are_equivalent_wrt f,g implies ex f, g being one-to-one Function st S2,S1 are_equivalent_wrt f,g )
given f, g being one-to-one Function such that A1: S1,S2 are_equivalent_wrt f,g ; :: thesis: ex f, g being one-to-one Function st S2,S1 are_equivalent_wrt f,g
take f " ; :: thesis: ex g being one-to-one Function st S2,S1 are_equivalent_wrt f " ,g
take g " ; :: thesis: S2,S1 are_equivalent_wrt f " ,g "
thus S2,S1 are_equivalent_wrt f " ,g " by A1, Th27; :: thesis: verum