let J be non empty non void Signature; :: thesis: for S being J -extension Signature

for T being MSAlgebra over J

for Q being MSAlgebra over S st Q is T -extension holds

for x being object st x in the carrier of J holds

the Sorts of T . x = the Sorts of Q . x

let S be J -extension Signature; :: thesis: for T being MSAlgebra over J

for Q being MSAlgebra over S st Q is T -extension holds

for x being object st x in the carrier of J holds

the Sorts of T . x = the Sorts of Q . x

J is Subsignature of S by Def2;

then A1: id the carrier of J, id the carrier' of J form_morphism_between J,S by INSTALG1:def 2;

let T be MSAlgebra over J; :: thesis: for Q being MSAlgebra over S st Q is T -extension holds

for x being object st x in the carrier of J holds

the Sorts of T . x = the Sorts of Q . x

let Q be MSAlgebra over S; :: thesis: ( Q is T -extension implies for x being object st x in the carrier of J holds

the Sorts of T . x = the Sorts of Q . x )

assume A2: Q | J = MSAlgebra(# the Sorts of T, the Charact of T #) ; :: according to AOFA_L00:def 19 :: thesis: for x being object st x in the carrier of J holds

the Sorts of T . x = the Sorts of Q . x

Q | J = Q | (J,(id the carrier of J),(id the carrier' of J)) by INSTALG1:def 4;

then A3: ( the Sorts of T = the Sorts of Q * (id the carrier of J) & dom (id the carrier of J) = the carrier of J ) by A1, A2, INSTALG1:def 3;

let x be object ; :: thesis: ( x in the carrier of J implies the Sorts of T . x = the Sorts of Q . x )

assume A4: x in the carrier of J ; :: thesis: the Sorts of T . x = the Sorts of Q . x

hence the Sorts of T . x = the Sorts of Q . ((id the carrier of J) . x) by A3, FUNCT_1:13

.= the Sorts of Q . x by A4, FUNCT_1:17 ;

:: thesis: verum

for T being MSAlgebra over J

for Q being MSAlgebra over S st Q is T -extension holds

for x being object st x in the carrier of J holds

the Sorts of T . x = the Sorts of Q . x

let S be J -extension Signature; :: thesis: for T being MSAlgebra over J

for Q being MSAlgebra over S st Q is T -extension holds

for x being object st x in the carrier of J holds

the Sorts of T . x = the Sorts of Q . x

J is Subsignature of S by Def2;

then A1: id the carrier of J, id the carrier' of J form_morphism_between J,S by INSTALG1:def 2;

let T be MSAlgebra over J; :: thesis: for Q being MSAlgebra over S st Q is T -extension holds

for x being object st x in the carrier of J holds

the Sorts of T . x = the Sorts of Q . x

let Q be MSAlgebra over S; :: thesis: ( Q is T -extension implies for x being object st x in the carrier of J holds

the Sorts of T . x = the Sorts of Q . x )

assume A2: Q | J = MSAlgebra(# the Sorts of T, the Charact of T #) ; :: according to AOFA_L00:def 19 :: thesis: for x being object st x in the carrier of J holds

the Sorts of T . x = the Sorts of Q . x

Q | J = Q | (J,(id the carrier of J),(id the carrier' of J)) by INSTALG1:def 4;

then A3: ( the Sorts of T = the Sorts of Q * (id the carrier of J) & dom (id the carrier of J) = the carrier of J ) by A1, A2, INSTALG1:def 3;

let x be object ; :: thesis: ( x in the carrier of J implies the Sorts of T . x = the Sorts of Q . x )

assume A4: x in the carrier of J ; :: thesis: the Sorts of T . x = the Sorts of Q . x

hence the Sorts of T . x = the Sorts of Q . ((id the carrier of J) . x) by A3, FUNCT_1:13

.= the Sorts of Q . x by A4, FUNCT_1:17 ;

:: thesis: verum