theorem Th22: :: AOFA_L00:23

for J being non void Signature
for S being non void b₁ -extension Signature
for A1, A2 being MSAlgebra over S st MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of A2, the Charact of A2 #) holds
A1 | J = A2 | J