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

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