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