let S be non empty non void ManySortedSign ; :: thesis: for s being SortSymbol of S
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
for i being object holds
( i in (FreeGen T) . s iff ex x being Element of X . s st i = x -term )
let s be SortSymbol of S; :: 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
for i being object holds
( i in (FreeGen T) . s iff ex x being Element of X . s st i = x -term )
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
for i being object holds
( i in (FreeGen T) . s iff ex x being Element of X . s st i = x -term )
let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S; :: thesis: for i being object holds
( i in (FreeGen T) . s iff ex x being Element of X . s st i = x -term )
let i be object ; :: thesis: ( i in (FreeGen T) . s iff ex x being Element of X . s st i = x -term )
A3: ( (FreeGen T) . s = FreeGen (s,X) & i is set ) by TARSKI:1, MSAFREE:def 16;

hereby :: thesis: ( ex x being Element of X . s st i = x -term implies i in (FreeGen T) . s )

assume i in (FreeGen T) . s ; :: thesis: ex x being Element of X . s st i = x -term
then consider x being set such that
A2: ( x in X . s & i = root-tree [x,s] ) by A3, MSAFREE:def 15;
reconsider x = x as Element of X . s by A2;
take x = x; :: thesis: i = x -term
thus i = x -term by A2; :: thesis: verum

end;

thus ( ex x being Element of X . s st i = x -term implies i in (FreeGen T) . s ) by A3, MSAFREE:def 15; :: thesis: verum