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