let S be ManySortedSign ; :: thesis: for o being set holds S variables_in ([o,the carrier of S] -tree {} ) = [0] the carrier of S
let o be set ; :: thesis: S variables_in ([o,the carrier of S] -tree {} ) = [0] the carrier of S

now

let s be set ; :: thesis: ( s in the carrier of S implies (S variables_in ([o,the carrier of S] -tree {} )) . s = ([0] the carrier of S) . s )
assume A1: s in the carrier of S ; :: thesis: (S variables_in ([o,the carrier of S] -tree {} )) . s = ([0] the carrier of S) . s

now

let x be set ; :: thesis: ( x in (S variables_in ([o,the carrier of S] -tree {} )) . s iff x in ([0] the carrier of S) . s )
rng {} = {} ;
then ( x in (S variables_in ([o,the carrier of S] -tree {} )) . s iff ex q being DecoratedTree st
( q in {} & x in (S variables_in q) . s ) ) by A1, MSAFREE3:12;
hence ( x in (S variables_in ([o,the carrier of S] -tree {} )) . s iff x in ([0] the carrier of S) . s ) by PBOOLE:5; :: thesis: verum

end;

hence (S variables_in ([o,the carrier of S] -tree {} )) . s = ([0] the carrier of S) . s by TARSKI:2; :: thesis: verum

end;

hence S variables_in ([o,the carrier of S] -tree {} ) = [0] the carrier of S by PBOOLE:3; :: thesis: verum