let S be non void Signature; :: thesis: for Y being V8() 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)) . iff rng p c= Union (S -Terms (X,Y)) )

let Y be V8() 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)) . 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)) . 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)) . 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)) . 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)) . = { 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)) . )
assume (Sym (o,Y)) -tree p in (S -Terms (X,Y)) . ; :: 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 ;
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 () . z c= X . z )
assume A10: z in the carrier of S ; :: thesis: () . z c= X . z
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in () . z or a in X . z )
assume a in () . z ; :: thesis: a in X . z
then A11: a in () . z by A4, A6, A8, A10, Th11;
(variables_in t) . z c= X . z by ;
hence a in X . z by A11; :: thesis: verum
end;
set sq = the_sort_of q;
(S -Terms (X,Y)) . () = { 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)) . () by A9;
hence y in Union (S -Terms (X,Y)) by ; :: 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)) .
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 () . z by ;
consider y being object such that
A17: y in the carrier of S and
A18: q in (S -Terms (X,Y)) . y by ;
(S -Terms (X,Y)) . y = { t9 where t9 is Term of S,Y : ( the_sort_of t9 = y & variables_in t9 c= X ) } by ;
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 ;
hence x in X . z by ; :: 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)) . by ; :: thesis: verum