let S, S' be non void Signature; :: thesis: for A being non-empty disjoint_valued MSAlgebra of S st A is Algebra of S' holds
S is Extension of S'
let A be non-empty disjoint_valued MSAlgebra of S; :: thesis: ( A is Algebra of S' implies S is Extension of S' )
assume A is Algebra of S' ; :: thesis: S is Extension of S'
then consider E being non void Extension of S' such that
A1: A is feasible MSAlgebra of E by Def7;
A2: S' is Subsignature of E by Def5;
A3: ManySortedSign(# the carrier of S,the carrier' of S,the Arity of S,the ResultSort of S #) = ManySortedSign(# the carrier of E,the carrier' of E,the Arity of E,the ResultSort of E #) by A1, Th65;
then A4: the ResultSort of S' c= the ResultSort of S by A2, INSTALG1:12;
the Arity of S' c= the Arity of S by A2, A3, INSTALG1:12;
hence S' is Subsignature of S by A2, A3, A4, INSTALG1:11, INSTALG1:14; :: according to ALGSPEC1:def 5 :: thesis: verum