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;
A2: {} * 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 A2, PUA2MSS1:def 13, RELAT_1:60, RELAT_1:81; :: thesis: verum