let S be non empty non void ManySortedSign ; for X being non-empty ManySortedSet of the carrier of S
for A being b1,S -terms all_vars_including inheriting_operations free_in_itself vf-free VarMSAlgebra over S
for s being SortSymbol of S
for t being Element of A,s holds vf t is ManySortedSubset of FreeGen X
let X be non-empty ManySortedSet of the carrier of S; for A being X,S -terms all_vars_including inheriting_operations free_in_itself vf-free VarMSAlgebra over S
for s being SortSymbol of S
for t being Element of A,s holds vf t is ManySortedSubset of FreeGen X
let A be X,S -terms all_vars_including inheriting_operations free_in_itself vf-free VarMSAlgebra over S; for s being SortSymbol of S
for t being Element of A,s holds vf t is ManySortedSubset of FreeGen X
let s be SortSymbol of S; for t being Element of A,s holds vf t is ManySortedSubset of FreeGen X
let t be Element of A,s; vf t is ManySortedSubset of FreeGen X
let x be object ; PBOOLE:def 2,PBOOLE:def 18 ( not x in the carrier of S or (vf t) . x c= (FreeGen X) . x )
assume
x in the carrier of S
; (vf t) . x c= (FreeGen X) . x
then reconsider r = x as SortSymbol of S ;
let y be object ; TARSKI:def 3 ( not y in (vf t) . x or y in (FreeGen X) . x )
assume
y in (vf t) . x
; y in (FreeGen X) . x
then
y in { (t | p) where p is Element of dom t : ((t | p) . {}) `2 = r }
by Def11;
then consider p being Element of dom t such that
A1:
( y = t | p & ((t | p) . {}) `2 = r )
;
t is Element of the Sorts of A . s
;
then reconsider tp = t | p as Element of A by MSAFREE4:44;
A2:
tp is Term of S,X
by MSAFREE4:42;