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)) st t is compound holds
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)) st t is compound holds
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: ( t is compound implies ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st t = o -term p )
reconsider d = t as Term of S,X by MSAFREE4:42;
assume t . {} in [: the carrier' of S,{ the carrier of S}:] ; :: according to ABCMIZ_1:def 27 :: thesis: 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} & d . {} = [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: d = [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;
take a ; :: thesis: ex p being Element of Args (a,(Free (S,X))) st t = a -term p
take p ; :: thesis: t = a -term p
thus t = a -term p by A2; :: thesis: verum