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