let S be non empty non void ManySortedSign ; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for t being Element of (Free (S,X)) holds
( ex s being SortSymbol of S ex x being Element of X . s st t = x -term or ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st t = o -term p )
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for t being Element of (Free (S,X)) holds
( ex s being SortSymbol of S ex x being Element of X . s st t = x -term or ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st t = o -term p )
let t be Element of (Free (S,X)); :: thesis: ( ex s being SortSymbol of S ex x being Element of X . s st t = x -term or ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st t = o -term p )
reconsider u = t as Term of S,X by MSAFREE4:42;

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

suppose ex s being SortSymbol of S ex x being Element of X . s st u . {} = [x,s] ; :: thesis: ( ex s being SortSymbol of S ex x being Element of X . s st t = x -term or ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st t = o -term p )

then consider s being SortSymbol of S, x being Element of X . s such that
A0: u . {} = [x,s] ;
( u = root-tree [x,s] & root-tree [x,s] = x -term ) by A0, MSATERM:5;
hence ( ex s being SortSymbol of S ex x being Element of X . s st t = x -term or ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st t = o -term p ) ; :: thesis: verum

end;

suppose u . {} in [: the carrier' of S,{ the carrier of S}:] ; :: thesis: ( ex s being SortSymbol of S ex x being Element of X . s st t = x -term or ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st t = o -term p )

then consider a, b being object such that
A1: ( a in the carrier' of S & b in { the carrier of S} & u . {} = [a,b] ) by ZFMISC_1:def 2;
reconsider a = a as OperSymbol of S by A1;
b = the carrier of S by A1, TARSKI:def 1;
then consider p being ArgumentSeq of Sym (a,X) such that
A2: u = [a, the carrier of S] -tree p by A1, MSATERM:10;
Free (S,X) = FreeMSA X by MSAFREE3:31;
then reconsider p = p as Element of Args (a,(Free (S,X))) by INSTALG1:1;
u = a -term p by A2;
hence ( ex s being SortSymbol of S ex x being Element of X . s st t = x -term or ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st t = o -term p ) ; :: thesis: verum

end;

end;