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

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