let T be Subsignature of S; :: thesis: T is feasible
set f = id the carrier of T;
set g = id the carrier' of T;
A1: dom (id the carrier' of T) = the carrier' of T ;
id the carrier of T, id the carrier' of T form_morphism_between T,S by Def2;
then A2: (id the carrier of T) * the ResultSort of T = the ResultSort of S * (id the carrier' of T) ;
assume the carrier of T = {} ; :: according to INSTALG1:def 1 :: thesis: the carrier' of T = {}
then A3: {} = the ResultSort of S * (id the carrier' of T) by A2;
( the carrier' of S = dom the ResultSort of S & rng (id the carrier' of T) = the carrier' of T ) by Th7;
hence the carrier' of T = {} by A3, A1, Th10, RELAT_1:27; :: thesis: verum