let J be non empty non void Signature; :: thesis: for S being J -extension Signature
for T being MSAlgebra over J
for Q1, Q2 being MSAlgebra over S st MSAlgebra(# the Sorts of Q1, the Charact of Q1 #) = MSAlgebra(# the Sorts of Q2, the Charact of Q2 #) & Q1 is T -extension holds
Q2 is T -extension
let S be J -extension Signature; :: thesis: for T being MSAlgebra over J
for Q1, Q2 being MSAlgebra over S st MSAlgebra(# the Sorts of Q1, the Charact of Q1 #) = MSAlgebra(# the Sorts of Q2, the Charact of Q2 #) & Q1 is T -extension holds
Q2 is T -extension
A1: J is Subsignature of S by Def2;
let T be MSAlgebra over J; :: thesis: for Q1, Q2 being MSAlgebra over S st MSAlgebra(# the Sorts of Q1, the Charact of Q1 #) = MSAlgebra(# the Sorts of Q2, the Charact of Q2 #) & Q1 is T -extension holds
Q2 is T -extension
let Q1, Q2 be MSAlgebra over S; :: thesis: ( MSAlgebra(# the Sorts of Q1, the Charact of Q1 #) = MSAlgebra(# the Sorts of Q2, the Charact of Q2 #) & Q1 is T -extension implies Q2 is T -extension )
assume A2: MSAlgebra(# the Sorts of Q1, the Charact of Q1 #) = MSAlgebra(# the Sorts of Q2, the Charact of Q2 #) ; :: thesis: ( not Q1 is T -extension or Q2 is T -extension )
assume A3: Q1 | J = MSAlgebra(# the Sorts of T, the Charact of T #) ; :: according to AOFA_L00:def 19 :: thesis: Q2 is T -extension
( Q1 | J = Q1 | (J,(id the carrier of J),(id the carrier' of J)) & Q2 | J = Q2 | (J,(id the carrier of J),(id the carrier' of J)) ) by INSTALG1:def 4;
hence Q2 | J = MSAlgebra(# the Sorts of T, the Charact of T #) by A3, A1, A2, INSTALG1:def 2, INSTALG1:21; :: according to AOFA_L00:def 19 :: thesis: verum