let S be empty void ManySortedSign ; :: thesis: id the carrier of S, id the carrier' of S form_morphism_between S,S
set f = id the carrier of S;
( {} * the ResultSort of S = the ResultSort of S * {} & ( for o being set
for p being Function st o in the carrier' of S & p = the Arity of S . o holds
(id the carrier of S) * p = the Arity of S . ((id the carrier of S) . o) ) ) ;
hence id the carrier of S, id the carrier' of S form_morphism_between S,S by PUA2MSS1:def 12, RELAT_1:38; :: thesis: verum