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 x being Element of X . s
for T being b₂,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds x -term in T
let s be SortSymbol of S; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for x being Element of X . s
for T being b₁,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds x -term in T
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for x being Element of X . s
for T being X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds x -term in T
let x be Element of X . s; :: thesis: for T being X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds x -term in T
let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S; :: thesis: x -term in T
( x -term in FreeGen (s,X) & FreeGen (s,X) = (FreeGen T) . s & (FreeGen T) . s c= the Sorts of T . s ) by PBOOLE:def 2, PBOOLE:def 18, MSAFREE:def 15, MSAFREE:def 16;
then x -term is Element of the Sorts of T . s ;
hence x -term in Union the Sorts of T ; :: according to MSAFREE5:def 2 :: thesis: verum