:: deftheorem Def17 defines -extension AOFA_L00:def 19 :
for J, S being non empty Signature
for T being MSAlgebra over J
for Q being MSAlgebra over S holds
( Q is T -extension iff Q | J = MSAlgebra(# the Sorts of T, the Charact of T #) );