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)) . (the_result_sort_of o) 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)) . (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;

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

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

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; :: 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) )

set t = (Sym (o,Y)) -tree p;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

end;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

(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;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

set sq = the_sort_of q;
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;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

(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

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

the_sort_of ((Sym (o,Y)) -tree p) = the_result_sort_of o
by MSATERM:20;
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;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

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