let S, T be Signature; :: thesis: ( S is empty implies T is Extension of S )
assume A1: the carrier of S is empty ; :: according to STRUCT_0:def 1 :: thesis: T is Extension of S
then the carrier' of S = {} by INSTALG1:def 1;
then ( the Arity of S = {} & the ResultSort of S = {} ) ;
then ( the carrier of S c= the carrier of T & the Arity of S c= the Arity of T & the ResultSort of S c= the ResultSort of T ) by A1, XBOOLE_1:2;
hence S is Subsignature of T by INSTALG1:14; :: according to ALGSPEC1:def 5 :: thesis: verum