let S be non void Signature; 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)) . (the_result_sort_of o) iff rng p c= Union (S -Terms (X,Y)) )
let Y be 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)) . (the_result_sort_of o) iff rng p c= Union (S -Terms (X,Y)) )
let X be 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 o be 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 p be ArgumentSeq of Sym (o,Y); ( (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 ( 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)
;
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))
verumproof
let y be
object ;
TARSKI:def 3 ( not y in rng p or y in Union (S -Terms (X,Y)) )
assume A6:
y in rng p
;
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
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;
verum
end;
end;
set t = (Sym (o,Y)) -tree p;
assume A12:
rng p c= Union (S -Terms (X,Y))
; (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 ;
PBOOLE:def 2 ( 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
;
(variables_in ((Sym (o,Y)) -tree p)) . z c= X . z
let x be
object ;
TARSKI:def 3 ( 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
;
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;
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; verum