set A = the non-empty T -extension MSAlgebra over S;
set f = the ManySortedMSSet of the Sorts of the non-empty T -extension MSAlgebra over S,X extended_by ({}, the carrier of S);
the ManySortedMSSet of the Sorts of the non-empty T -extension MSAlgebra over S,X extended_by ({}, the carrier of S) is ManySortedMSSet of the Sorts of the non-empty T -extension MSAlgebra over S, the Sorts of the non-empty T -extension MSAlgebra over S

proof

let i, a be set ; :: according to AOFA_A00:def 7 :: thesis: ( not i in the carrier of S or not a in the Sorts of the non-empty T -extension MSAlgebra over S . i or ( the ManySortedMSSet of the Sorts of the non-empty T -extension MSAlgebra over S,X extended_by ({}, the carrier of S) . i) . a is ManySortedSubset of the Sorts of the non-empty T -extension MSAlgebra over S )
assume ( i in the carrier of S & a in the Sorts of the non-empty T -extension MSAlgebra over S . i ) ; :: thesis: ( the ManySortedMSSet of the Sorts of the non-empty T -extension MSAlgebra over S,X extended_by ({}, the carrier of S) . i) . a is ManySortedSubset of the Sorts of the non-empty T -extension MSAlgebra over S
then reconsider fia = ( the ManySortedMSSet of the Sorts of the non-empty T -extension MSAlgebra over S,X extended_by ({}, the carrier of S) . i) . a as ManySortedSubset of X extended_by ({}, the carrier of S) by AOFA_A00:def 8;
fia c= the Sorts of the non-empty T -extension MSAlgebra over S

proof

let y be object ; :: according to PBOOLE:def 2 :: thesis: ( not y in the carrier of S or fia . y c= the Sorts of the non-empty T -extension MSAlgebra over S . y )
assume y in the carrier of S ; :: thesis: fia . y c= the Sorts of the non-empty T -extension MSAlgebra over S . y
then A1: fia . y c= (X extended_by ({}, the carrier of S)) . y by PBOOLE:def 2, PBOOLE:def 18;
A2: J is Subsignature of S by Def2;
then A3: ( dom X = the carrier of J & the carrier of J c= the carrier of S ) by PARTFUN1:def 2, INSTALG1:10;
then A4: ( X extended_by ({}, the carrier of S) = ( the carrier of S --> {}) +* (X | the carrier of S) & ( the carrier of S --> {}) +* (X | the carrier of S) = ( the carrier of S --> {}) +* X ) by RELAT_1:68;
( the non-empty T -extension MSAlgebra over S | (J,(id the carrier of J),(id the carrier' of J)) = the non-empty T -extension MSAlgebra over S | J & the non-empty T -extension MSAlgebra over S | J = MSAlgebra(# the Sorts of T, the Charact of T #) & id the carrier of J, id the carrier' of J form_morphism_between J,S ) by A2, Def17, INSTALG1:def 2, INSTALG1:def 4;
then A5: the Sorts of the non-empty T -extension MSAlgebra over S * (id the carrier of J) = the Sorts of T by INSTALG1:def 3;

per cases ( y in the carrier of J or y nin the carrier of J ) ;

suppose A6: y in the carrier of J ; :: thesis: fia . y c= the Sorts of the non-empty T -extension MSAlgebra over S . y

( (X extended_by ({}, the carrier of S)) . y = X . y & X . y c= the Sorts of T . y & the Sorts of T . y = the Sorts of the non-empty T -extension MSAlgebra over S . ((id the carrier of J) . y) & the Sorts of the non-empty T -extension MSAlgebra over S . ((id the carrier of J) . y) = the Sorts of the non-empty T -extension MSAlgebra over S . y ) by A6, A3, A4, A5, FUNCT_4:13, PBOOLE:def 2, PBOOLE:def 18, FUNCT_1:17, FUNCT_2:15;
hence fia . y c= the Sorts of the non-empty T -extension MSAlgebra over S . y by A1; :: thesis: verum

end;

suppose y nin the carrier of J ; :: thesis: fia . y c= the Sorts of the non-empty T -extension MSAlgebra over S . y

then (X extended_by ({}, the carrier of S)) . y = ( the carrier of S --> {}) . y by A3, A4, FUNCT_4:11
.= {} ;
hence fia . y c= the Sorts of the non-empty T -extension MSAlgebra over S . y by A1; :: thesis: verum

end;

end;

end;

hence ( the ManySortedMSSet of the Sorts of the non-empty T -extension MSAlgebra over S,X extended_by ({}, the carrier of S) . i) . a is ManySortedSubset of the Sorts of the non-empty T -extension MSAlgebra over S by PBOOLE:def 18; :: thesis: verum

end;

then reconsider f = the ManySortedMSSet of the Sorts of the non-empty T -extension MSAlgebra over S,X extended_by ({}, the carrier of S) as ManySortedMSSet of the Sorts of the non-empty T -extension MSAlgebra over S, the Sorts of the non-empty T -extension MSAlgebra over S ;
set Y = X extended_by ({}, the carrier of S);
set g = the sort-preserving Function of [:(Union the Sorts of the non-empty T -extension MSAlgebra over S),(Union [|(X extended_by ({}, the carrier of S)), the Sorts of the non-empty T -extension MSAlgebra over S|]):],(Union the Sorts of the non-empty T -extension MSAlgebra over S);
set eq = the Function of (Union [| the Sorts of T, the Sorts of T|]),( the Sorts of the non-empty T -extension MSAlgebra over S . the formula-sort of S);
take L = LanguageStr(# the Sorts of the non-empty T -extension MSAlgebra over S, the Charact of the non-empty T -extension MSAlgebra over S,f, the sort-preserving Function of [:(Union the Sorts of the non-empty T -extension MSAlgebra over S),(Union [|(X extended_by ({}, the carrier of S)), the Sorts of the non-empty T -extension MSAlgebra over S|]):],(Union the Sorts of the non-empty T -extension MSAlgebra over S), the Function of (Union [| the Sorts of T, the Sorts of T|]),( the Sorts of the non-empty T -extension MSAlgebra over S . the formula-sort of S) #); :: thesis: ( L is X extended_by ({}, the carrier of S) -vf-yielding & L is non-empty & L is language & L is T -extension )
thus the free-vars of L is ManySortedMSSet of the Sorts of L,X extended_by ({}, the carrier of S) ; :: according to AOFA_L00:def 9 :: thesis: ( L is non-empty & L is language & L is T -extension )
thus the Sorts of L is non-empty ; :: according to MSUALG_1:def 3 :: thesis: ( L is language & L is T -extension )
thus not the Sorts of L . the formula-sort of S is empty ; :: according to AOFA_L00:def 20 :: thesis: L is T -extension
MSAlgebra(# the Sorts of L, the Charact of L #) = MSAlgebra(# the Sorts of the non-empty T -extension MSAlgebra over S, the Charact of the non-empty T -extension MSAlgebra over S #) ;
hence L | J = the non-empty T -extension MSAlgebra over S | J by Th22
.= MSAlgebra(# the Sorts of T, the Charact of T #) by Def17 ;
:: according to AOFA_L00:def 19 :: thesis: verum