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

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