let S be non empty non void ManySortedSign ; :: thesis: for X being V2() ManySortedSet of
for t being Term of S,X st not t is trivial holds
ex o being OperSymbol of S st t . {} = [o,the carrier of S]
let X be V2() ManySortedSet of ; :: thesis: for t being Term of S,X st not t is trivial 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 trivial implies ex o being OperSymbol of S st t . {} = [o,the carrier of S] )
assume A1: not t is trivial ; :: 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 set such that
A3: ( o in the carrier' of S & 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 A3, TARSKI:def 1; :: thesis: verum

end;

end;