let S be non empty non void ManySortedSign ; :: thesis: for s being SortSymbol of S
for X being V5() ManySortedSet of the carrier of S
for T being b2,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 V5() ManySortedSet of the carrier of S
for T being b1,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 V5() 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