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:11;
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:1; :: thesis: verum

end;

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