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

now :: thesis: for s being object st s in the carrier of S holds
(S variables_in ([o, the carrier of S] -tree {})) . s = (EmptyMS the carrier of S) . s

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

now :: thesis: for x being object holds
( x in (S variables_in ([o, the carrier of S] -tree {})) . s iff x in (EmptyMS the carrier of S) . s )

let x be object ; :: thesis: ( x in (S variables_in ([o, the carrier of S] -tree {})) . s iff x in (EmptyMS 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 (EmptyMS the carrier of S) . s ) ; :: thesis: verum

end;

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

end;

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