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

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 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,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

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 ;
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

end;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

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
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;

end;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 )
;

end;

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;hence fia . y c= the Sorts of the non-empty T -extension MSAlgebra over S . y by A1; :: thesis: verum

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;.= {} ;

hence fia . y c= the Sorts of the non-empty T -extension MSAlgebra over S . y by A1; :: thesis: verum

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 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