let J be non empty non void Signature; 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; 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; 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; ( 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 #)
; ( not Q1 is T -extension or Q2 is T -extension )
assume A3:
Q1 | J = MSAlgebra(# the Sorts of T, the Charact of T #)
; AOFA_L00:def 19 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; AOFA_L00:def 19 verum