take id the Sorts of A ; :: thesis: id the Sorts of A is_homomorphism A,A
thus id the Sorts of A is_homomorphism A,A by MSUALG_3:9; :: thesis: verum