let S be feasible ManySortedSign ; :: thesis: for T being Subsignature of S holds

( the carrier of T c= the carrier of S & the carrier' of T c= the carrier' of S )

let T be Subsignature of S; :: thesis: ( the carrier of T c= the carrier of S & the carrier' of T c= the carrier' of S )

set g = id the carrier' of T;

id the carrier of T, id the carrier' of T form_morphism_between T,S by Def2;

then ( rng (id the carrier of T) c= the carrier of S & rng (id the carrier' of T) c= the carrier' of S ) ;

hence ( the carrier of T c= the carrier of S & the carrier' of T c= the carrier' of S ) ; :: thesis: verum

( the carrier of T c= the carrier of S & the carrier' of T c= the carrier' of S )

let T be Subsignature of S; :: thesis: ( the carrier of T c= the carrier of S & the carrier' of T c= the carrier' of S )

set g = id the carrier' of T;

id the carrier of T, id the carrier' of T form_morphism_between T,S by Def2;

then ( rng (id the carrier of T) c= the carrier of S & rng (id the carrier' of T) c= the carrier' of S ) ;

hence ( the carrier of T c= the carrier of S & the carrier' of T c= the carrier' of S ) ; :: thesis: verum