let S be non 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;
set g = id the carrier' of S;
A1: ( rng (id the carrier of S) c= the carrier of S & rng (id the carrier' of S) c= the carrier' of S ) ;
A2: ( (id the carrier of S) * the ResultSort of S = {} & the ResultSort of S * (id the carrier' of S) = {} ) ;
A3: 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) ;
( dom (id the carrier of S) = the carrier of S & dom (id the carrier' of S) = the carrier' of S ) ;
hence id the carrier of S, id the carrier' of S form_morphism_between S,S by A1, A2, A3, PUA2MSS1:def 12; :: thesis: verum