let S be non empty non void ManySortedSign ; :: thesis: for X being V2() ManySortedSet of the carrier of S

for A being b_{1},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;

for A being b

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;

per cases
( tp . {} in [: the carrier' of S,{ the carrier of S}:] or ex s being SortSymbol of S ex v being Element of X . s st tp . {} = [v,s] )
by A2, MSATERM:2;

end;

suppose
tp . {} in [: the carrier' of S,{ the carrier of S}:]
; :: thesis: y in (FreeGen X) . x

then
r in { the carrier of S}
by A1, MCART_1:10;

then r = the carrier of S by TARSKI:def 1;

then r in r ;

hence y in (FreeGen X) . x ; :: thesis: verum

end;then r = the carrier of S by TARSKI:def 1;

then r in r ;

hence y in (FreeGen X) . x ; :: thesis: verum

suppose
ex s being SortSymbol of S ex v being Element of X . s st tp . {} = [v,s]
; :: thesis: y in (FreeGen X) . x

then consider s1 being SortSymbol of S, v being Element of X . s1 such that

A3: tp . {} = [v,s1] ;

tp = root-tree [v,s1] by A2, A3, MSATERM:5;

then tp in FreeGen (s1,X) by MSAFREE:def 15;

then tp in (FreeGen X) . s1 by MSAFREE:def 16;

hence y in (FreeGen X) . x by A1, A3; :: thesis: verum

end;A3: tp . {} = [v,s1] ;

tp = root-tree [v,s1] by A2, A3, MSATERM:5;

then tp in FreeGen (s1,X) by MSAFREE:def 15;

then tp in (FreeGen X) . s1 by MSAFREE:def 16;

hence y in (FreeGen X) . x by A1, A3; :: thesis: verum