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

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