let S be ManySortedSign ; :: thesis: for o being set
for t being DecoratedTree holds S variables_in ([o, the carrier of S] -tree <*t*>) = S variables_in t
let o be set ; :: thesis: for t being DecoratedTree holds S variables_in ([o, the carrier of S] -tree <*t*>) = S variables_in t
let t be DecoratedTree; :: thesis: S variables_in ([o, the carrier of S] -tree <*t*>) = S variables_in t

now :: thesis: for s being object st s in the carrier of S holds
(S variables_in ([o, the carrier of S] -tree <*t*>)) . s = (S variables_in t) . s

let s be object ; :: thesis: ( s in the carrier of S implies (S variables_in ([o, the carrier of S] -tree <*t*>)) . s = (S variables_in t) . s )
assume A1: s in the carrier of S ; :: thesis: (S variables_in ([o, the carrier of S] -tree <*t*>)) . s = (S variables_in t) . s
A2: t in {t} by TARSKI:def 1;

now :: thesis: for x being object holds
( x in (S variables_in ([o, the carrier of S] -tree <*t*>)) . s iff x in (S variables_in t) . s )

let x be object ; :: thesis: ( x in (S variables_in ([o, the carrier of S] -tree <*t*>)) . s iff x in (S variables_in t) . s )
rng <*t*> = {t} by FINSEQ_1:39;
then ( x in (S variables_in ([o, the carrier of S] -tree <*t*>)) . s iff ex q being DecoratedTree st
( q in {t} & x in (S variables_in q) . s ) ) by A1, MSAFREE3:11;
hence ( x in (S variables_in ([o, the carrier of S] -tree <*t*>)) . s iff x in (S variables_in t) . s ) by A2, TARSKI:def 1; :: thesis: verum

end;

hence (S variables_in ([o, the carrier of S] -tree <*t*>)) . s = (S variables_in t) . s by TARSKI:2; :: thesis: verum

end;

hence S variables_in ([o, the carrier of S] -tree <*t*>) = S variables_in t ; :: thesis: verum