let S be non empty non void ManySortedSign ; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for T being b₁,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds T deg<= 0 = Union (FreeGen T)
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for T being X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds T deg<= 0 = Union (FreeGen T)
let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S; :: thesis: T deg<= 0 = Union (FreeGen T)
A0: T deg<= 0 = { (x -term) where s is SortSymbol of S, x is Element of X . s : verum } by Th11;
thus T deg<= 0 c= Union (FreeGen T) :: according to XBOOLE_0:def 10 :: thesis: Union (FreeGen T) c= T deg<= 0

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in T deg<= 0 or x in Union (FreeGen T) )
assume x in T deg<= 0 ; :: thesis: x in Union (FreeGen T)
then consider s being SortSymbol of S, y being Element of X . s such that
A1: x = y -term by A0;
x in FreeGen (s,X) by A1, MSAFREE:def 15;
then ( x in (FreeGen T) . s & s in the carrier of S & the carrier of S = dom (FreeGen T) ) by PARTFUN1:def 2, MSAFREE:def 16;
hence x in Union (FreeGen T) by CARD_5:2; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Union (FreeGen T) or a in T deg<= 0 )
assume a in Union (FreeGen T) ; :: thesis: a in T deg<= 0
then consider b being object such that
A2: ( b in dom (FreeGen T) & a in (FreeGen T) . b ) by CARD_5:2;
reconsider b = b as SortSymbol of S by A2;
a in FreeGen (b,X) by A2, MSAFREE:def 16;
then consider y being set such that
A3: ( y in X . b & a = root-tree [y,b] ) by MSAFREE:def 15;
reconsider y = y as Element of X . b by A3;
a = y -term by A3;
hence a in T deg<= 0 by A0; :: thesis: verum