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, the Sorts of the non-empty T -extension MSAlgebra over S;
set g = the sort-preserving Function of [:(Union the Sorts of the non-empty T -extension MSAlgebra over S),(Union [|Y, 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, the ManySortedMSSet of the Sorts of the non-empty T -extension MSAlgebra over S, the Sorts of the non-empty T -extension MSAlgebra over S, the sort-preserving Function of [:(Union the Sorts of the non-empty T -extension MSAlgebra over S),(Union [|Y, 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 non-empty & L is language & L is T -extension )
thus the Sorts of L is V2() ; :: 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