let S, S9 be non void Signature; :: thesis: for A being non-empty disjoint_valued MSAlgebra of S st A is Algebra of S9 holds
S is Extension of S9
let A be non-empty disjoint_valued MSAlgebra of 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 of 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, Th65;
then A4: the ResultSort of S9 c= the ResultSort of S by A2, INSTALG1:12;
the Arity of S9 c= the Arity of S by A2, A3, INSTALG1:12;
hence S9 is Subsignature of S by A2, A3, A4, INSTALG1:11, INSTALG1:14; :: according to ALGSPEC1:def 5 :: thesis: verum