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;
( S' is Subsignature of E & 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, Def5, Th65;
then ( the carrier of S' c= the carrier of S & the Arity of S' c= the Arity of S & the ResultSort of S' c= the ResultSort of S ) by INSTALG1:11, INSTALG1:12;
hence S' is Subsignature of S by INSTALG1:14; :: according to ALGSPEC1:def 5 :: thesis: verum