let S be Signature; :: thesis: for E being non empty Signature
for A being MSAlgebra of 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 of 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 of 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 ) )
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
A1: A is feasible MSAlgebra of ES by Def7;
reconsider B = A as MSAlgebra of ES by A1;
A2: S is Subsignature of ES by Def5;
( dom the Sorts of B = the carrier of ES & dom the Sorts of A = the carrier of E ) by PARTFUN1:def 4;
hence the carrier of S c= the carrier of E by A2, INSTALG1:11; :: thesis: the carrier' of S c= the carrier' of E
( dom the Charact of B = the carrier' of ES & dom the Charact of A = the carrier' of E ) by PARTFUN1:def 4;
hence the carrier' of S c= the carrier' of E by A2, INSTALG1:11; :: thesis: verum