let S be non empty non void ManySortedSign ; :: thesis: for X being V2() ManySortedSet of the carrier of S
for A being b₁,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 V2() ManySortedSet of the carrier of S; :: thesis: 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; :: thesis: 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; :: thesis: for t being Element of A,s holds vf t is ManySortedSubset of FreeGen X
let t be Element of A,s; :: thesis: vf t is ManySortedSubset of FreeGen X
let x be object ; :: according to PBOOLE:def 2,PBOOLE:def 18 :: thesis: ( not x in the carrier of S or (vf t) . x c= (FreeGen X) . x )
assume x in the carrier of S ; :: thesis: (vf t) . x c= (FreeGen X) . x
then reconsider r = x as SortSymbol of S ;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (vf t) . x or y in (FreeGen X) . x )
assume y in (vf t) . x ; :: thesis: 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;