let S be non void Signature; :: thesis: for Y being V5() ManySortedSet of
for X being ManySortedSet of
for o being OperSymbol of S
for p being ArgumentSeq of Sym o,Y holds
( (Sym o,Y) -tree p in (S -Terms X,Y) . (the_result_sort_of o) iff rng p c= Union (S -Terms X,Y) )
let Y be V5() ManySortedSet of ; :: thesis: for X being ManySortedSet of
for o being OperSymbol of S
for p being ArgumentSeq of Sym o,Y holds
( (Sym o,Y) -tree p in (S -Terms X,Y) . (the_result_sort_of o) iff rng p c= Union (S -Terms X,Y) )
let X be ManySortedSet of ; :: thesis: for o being OperSymbol of S
for p being ArgumentSeq of Sym o,Y holds
( (Sym o,Y) -tree p in (S -Terms X,Y) . (the_result_sort_of o) iff rng p c= Union (S -Terms X,Y) )
let o be OperSymbol of S; :: thesis: for p being ArgumentSeq of Sym o,Y holds
( (Sym o,Y) -tree p in (S -Terms X,Y) . (the_result_sort_of o) iff rng p c= Union (S -Terms X,Y) )
let p be ArgumentSeq of Sym o,Y; :: thesis: ( (Sym o,Y) -tree p in (S -Terms X,Y) . (the_result_sort_of o) iff rng p c= Union (S -Terms X,Y) )
set s = the_result_sort_of o;
A1: dom (S -Terms X,Y) = the carrier of S by PARTFUN1:def 4;
A2: (S -Terms X,Y) . (the_result_sort_of o) = { t where t is Term of S,Y : ( the_sort_of t = the_result_sort_of o & variables_in t c= X ) } by Def6;
A3: Sym o,Y = [o,the carrier of S] by MSAFREE:def 11;

hereby :: thesis: ( rng p c= Union (S -Terms X,Y) implies (Sym o,Y) -tree p in (S -Terms X,Y) . (the_result_sort_of o) )

assume (Sym o,Y) -tree p in (S -Terms X,Y) . (the_result_sort_of o) ; :: thesis: rng p c= Union (S -Terms X,Y)
then consider t being Term of S,Y such that
A4: ( [o,the carrier of S] -tree p = t & the_sort_of t = the_result_sort_of o & variables_in t c= X ) by A2, A3;
thus rng p c= Union (S -Terms X,Y) :: thesis: verum

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng p or y in Union (S -Terms X,Y) )
assume A5: y in rng p ; :: thesis: y in Union (S -Terms X,Y)
then consider x being set such that
A6: ( x in dom p & y = p . x ) by FUNCT_1:def 5;
reconsider x = x as Nat by A6;
reconsider q = p . x as Term of S,Y by A6, MSATERM:22;
set sq = the_sort_of q;
A7: (S -Terms X,Y) . (the_sort_of q) = { t' where t' is Term of S,Y : ( the_sort_of t' = the_sort_of q & variables_in t' c= X ) } by Def6;
variables_in q c= X

proof

let z be set ; :: according to PBOOLE:def 5 :: thesis: ( not z in the carrier of S or (variables_in q) . z c= X . z )
assume A8: z in the carrier of S ; :: thesis: (variables_in q) . z c= X . z
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in (variables_in q) . z or a in X . z )
assume a in (variables_in q) . z ; :: thesis: a in X . z
then ( a in (variables_in t) . z & (variables_in t) . z c= X . z ) by A4, A5, A6, A8, Th12, PBOOLE:def 5;
hence a in X . z ; :: thesis: verum

end;

then q in (S -Terms X,Y) . (the_sort_of q) by A7;
hence y in Union (S -Terms X,Y) by A1, A6, CARD_5:10; :: thesis: verum

end;

end;

assume A9: rng p c= Union (S -Terms X,Y) ; :: thesis: (Sym o,Y) -tree p in (S -Terms X,Y) . (the_result_sort_of o)
set t = (Sym o,Y) -tree p;
A10: the_sort_of ((Sym o,Y) -tree p) = the_result_sort_of o by MSATERM:20;
variables_in ((Sym o,Y) -tree p) c= X

proof

let z be set ; :: according to PBOOLE:def 5 :: thesis: ( not z in the carrier of S or (variables_in ((Sym o,Y) -tree p)) . z c= X . z )
assume A11: z in the carrier of S ; :: thesis: (variables_in ((Sym o,Y) -tree p)) . z c= X . z
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (variables_in ((Sym o,Y) -tree p)) . z or x in X . z )
assume x in (variables_in ((Sym o,Y) -tree p)) . z ; :: thesis: x in X . z
then consider q being DecoratedTree such that
A12: ( q in rng p & x in (S variables_in q) . z ) by A3, A11, Th12;
consider y being set such that
A13: ( y in the carrier of S & q in (S -Terms X,Y) . y ) by A1, A9, A12, CARD_5:10;
(S -Terms X,Y) . y = { t' where t' is Term of S,Y : ( the_sort_of t' = y & variables_in t' c= X ) } by A13, Def6;
then consider t' being Term of S,Y such that
A14: ( q = t' & the_sort_of t' = y & variables_in t' c= X ) by A13;
( (variables_in t') . z c= X . z & variables_in t' = S variables_in q ) by A11, A14, PBOOLE:def 5;
hence x in X . z by A12; :: thesis: verum

end;

hence (Sym o,Y) -tree p in (S -Terms X,Y) . (the_result_sort_of o) by A2, A10; :: thesis: verum