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

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