let J be non void Signature; :: thesis: for S being non void J -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
let S be non void J -extension Signature; :: thesis: 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
let A1, A2 be MSAlgebra over S; :: thesis: ( MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of A2, the Charact of A2 #) implies A1 | J = A2 | J )
assume A1: MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of A2, the Charact of A2 #) ; :: thesis: A1 | J = A2 | J
A2: ( A1 | J = A1 | (J,(id the carrier of J),(id the carrier' of J)) & A2 | J = A2 | (J,(id the carrier of J),(id the carrier' of J)) ) by INSTALG1:def 4;
J is Subsignature of S by Def2;
then id the carrier of J, id the carrier' of J form_morphism_between J,S by INSTALG1:def 2;
then ( the Sorts of (A1 | J) = the Sorts of A1 * (id the carrier of J) & the Sorts of (A2 | J) = the Sorts of A2 * (id the carrier of J) & the Charact of (A1 | J) = the Charact of A1 * (id the carrier' of J) & the Charact of (A2 | J) = the Charact of A2 * (id the carrier' of J) ) by A2, INSTALG1:def 3;
hence A1 | J = A2 | J by A1; :: thesis: verum