let S, S9 be non void Signature; :: thesis: for A being non-empty disjoint_valued MSAlgebra over S st A is Algebra of S9 holds
S is Extension of S9
let A be non-empty disjoint_valued MSAlgebra over S; :: thesis: ( A is Algebra of S9 implies S is Extension of S9 )
assume A is Algebra of S9 ; :: thesis: S is Extension of S9
then consider E being non void Extension of S9 such that
A1: A is feasible MSAlgebra over E by Def7;
A2: S9 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, Th62;
then A4: the ResultSort of S9 c= the ResultSort of S by A2, INSTALG1:11;
the Arity of S9 c= the Arity of S by A2, A3, INSTALG1:11;
hence S9 is Subsignature of S by A2, A3, A4, INSTALG1:10, INSTALG1:13; :: according to ALGSPEC1:def 5 :: thesis: verum