theorem Th25: :: INSTALG1:25

for S being non empty ManySortedSign
for A being MSAlgebra over S holds A | (S,(id the carrier of S),(id the carrier' of S)) = MSAlgebra(# the Sorts of A, the Charact of A #)