let S be non empty ManySortedSign ; :: thesis: ex f, g being one-to-one Function st S,S are_equivalent_wrt f,g
take id the carrier of S ; :: thesis: ex g being one-to-one Function st S,S are_equivalent_wrt id the carrier of S,g
take id the carrier' of S ; :: thesis: S,S are_equivalent_wrt id the carrier of S, id the carrier' of S
thus S,S are_equivalent_wrt id the carrier of S, id the carrier' of S by Th25; :: thesis: verum