let S be non empty non void ManySortedSign ; for s being SortSymbol of S
for X being V5() ManySortedSet of the carrier of S
for x being Element of X . s
for T being b2,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds x -term in T
let s be SortSymbol of S; for X being V5() ManySortedSet of the carrier of S
for x being Element of X . s
for T being b1,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds x -term in T
let X be V5() ManySortedSet of the carrier of S; 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; 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; 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
; MSAFREE5:def 2 verum