let S be non void Signature; :: thesis: for Y being non-empty ManySortedSet of the carrier of S
for X being ManySortedSet of the carrier of S
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 non-empty ManySortedSet of the carrier of S; :: thesis: for X being ManySortedSet of the carrier of S
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 the carrier of S; :: 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 2;
A2: Sym (o,Y) = [o, the carrier of S] by MSAFREE:def 9;
A3: (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 Def5;

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 and
the_sort_of t = the_result_sort_of o and
A5: variables_in t c= X by A3, A2;
thus rng p c= Union (S -Terms (X,Y)) :: thesis: verum

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng p or y in Union (S -Terms (X,Y)) )
assume A6: y in rng p ; :: thesis: y in Union (S -Terms (X,Y))
then consider x being object such that
A7: x in dom p and
A8: y = p . x by FUNCT_1:def 3;
reconsider x = x as Nat by A7;
reconsider q = p . x as Term of S,Y by A7, MSATERM:22;
A9: variables_in q c= X

proof

let z be object ; :: according to PBOOLE:def 2 :: thesis: ( not z in the carrier of S or (variables_in q) . z c= X . z )
assume A10: z in the carrier of S ; :: thesis: (variables_in q) . z c= X . z
let a be object ; :: 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 A11: a in (variables_in t) . z by A4, A6, A8, A10, Th11;
(variables_in t) . z c= X . z by A5, A10;
hence a in X . z by A11; :: thesis: verum

end;

set sq = the_sort_of q;
(S -Terms (X,Y)) . (the_sort_of q) = { t9 where t9 is Term of S,Y : ( the_sort_of t9 = the_sort_of q & variables_in t9 c= X ) } by Def5;
then q in (S -Terms (X,Y)) . (the_sort_of q) by A9;
hence y in Union (S -Terms (X,Y)) by A1, A8, CARD_5:2; :: thesis: verum

end;

end;

set t = (Sym (o,Y)) -tree p;
assume A12: rng p c= Union (S -Terms (X,Y)) ; :: thesis: (Sym (o,Y)) -tree p in (S -Terms (X,Y)) . (the_result_sort_of o)
A13: variables_in ((Sym (o,Y)) -tree p) c= X

proof

let z be object ; :: according to PBOOLE:def 2 :: thesis: ( not z in the carrier of S or (variables_in ((Sym (o,Y)) -tree p)) . z c= X . z )
assume A14: z in the carrier of S ; :: thesis: (variables_in ((Sym (o,Y)) -tree p)) . z c= X . z
let x be object ; :: 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
A15: q in rng p and
A16: x in (S variables_in q) . z by A2, A14, Th11;
consider y being object such that
A17: y in the carrier of S and
A18: q in (S -Terms (X,Y)) . y by A1, A12, A15, CARD_5:2;
(S -Terms (X,Y)) . y = { t9 where t9 is Term of S,Y : ( the_sort_of t9 = y & variables_in t9 c= X ) } by A17, Def5;
then consider t9 being Term of S,Y such that
A19: q = t9 and
the_sort_of t9 = y and
A20: variables_in t9 c= X by A18;
(variables_in t9) . z c= X . z by A14, A20;
hence x in X . z by A16, A19; :: thesis: verum

end;

the_sort_of ((Sym (o,Y)) -tree p) = the_result_sort_of o by MSATERM:20;
hence (Sym (o,Y)) -tree p in (S -Terms (X,Y)) . (the_result_sort_of o) by A3, A13; :: thesis: verum