let S be non empty non void ManySortedSign ; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for t being Term of S,X st not t is root holds
ex o being OperSymbol of S st t . {} = [o, the carrier of S]
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for t being Term of S,X st not t is root holds
ex o being OperSymbol of S st t . {} = [o, the carrier of S]
let t be Term of S,X; :: thesis: ( not t is root implies ex o being OperSymbol of S st t . {} = [o, the carrier of S] )
assume A1: not t is root ; :: thesis: ex o being OperSymbol of S st t . {} = [o, the carrier of S]

per cases ( ex s being SortSymbol of S ex v being Element of X . s st t . {} = [v,s] or t . {} in [: the carrier' of S,{ the carrier of S}:] ) by MSATERM:2;

suppose ex s being SortSymbol of S ex v being Element of X . s st t . {} = [v,s] ; :: thesis: ex o being OperSymbol of S st t . {} = [o, the carrier of S]

then consider s being SortSymbol of S, v being Element of X . s such that
A2: t . {} = [v,s] ;
t = root-tree [v,s] by A2, MSATERM:5;
hence ex o being OperSymbol of S st t . {} = [o, the carrier of S] by A1; :: thesis: verum

end;

suppose t . {} in [: the carrier' of S,{ the carrier of S}:] ; :: thesis: ex o being OperSymbol of S st t . {} = [o, the carrier of S]

then consider o, c being object such that
A3: o in the carrier' of S and
A4: ( c in { the carrier of S} & t . {} = [o,c] ) by ZFMISC_1:def 2;
reconsider o = o as OperSymbol of S by A3;
take o ; :: thesis: t . {} = [o, the carrier of S]
thus t . {} = [o, the carrier of S] by A4, TARSKI:def 1; :: thesis: verum

end;

end;