let S be Signature; :: thesis: for E being Extension of S
for A being Algebra of E holds A is Algebra of S
let E be Extension of S; :: thesis: for A being Algebra of E holds A is Algebra of S
let A be Algebra of E; :: thesis: A is Algebra of S
consider E9 being non void Extension of E such that
A1: A is feasible MSAlgebra over E9 by Def7;
E9 is Extension of S by Th46;
hence A is Algebra of S by A1, Def7; :: thesis: verum