let S be Signature; :: thesis: for E being non empty Signature
for A being MSAlgebra over E st A is Algebra of S holds
( the carrier of S c= the carrier of E & the carrier' of S c= the carrier' of E )
let E be non empty Signature; :: thesis: for A being MSAlgebra over E st A is Algebra of S holds
( the carrier of S c= the carrier of E & the carrier' of S c= the carrier' of E )
let A be MSAlgebra over E; :: thesis: ( A is Algebra of S implies ( the carrier of S c= the carrier of E & the carrier' of S c= the carrier' of E ) )
A1: dom the Charact of A = the carrier' of E by PARTFUN1:def 2;
assume A is Algebra of S ; :: thesis: ( the carrier of S c= the carrier of E & the carrier' of S c= the carrier' of E )
then consider ES being non void Extension of S such that
A2: A is feasible MSAlgebra over ES by Def7;
reconsider B = A as MSAlgebra over ES by A2;
A3: dom the Sorts of A = the carrier of E by PARTFUN1:def 2;
A4: S is Subsignature of ES by Def5;
dom the Sorts of B = the carrier of ES by PARTFUN1:def 2;
hence the carrier of S c= the carrier of E by A4, A3, INSTALG1:10; :: thesis: the carrier' of S c= the carrier' of E
dom the Charact of B = the carrier' of ES by PARTFUN1:def 2;
hence the carrier' of S c= the carrier' of E by A4, A1, INSTALG1:10; :: thesis: verum