let S be non empty non void ManySortedSign ; :: thesis: for V being V16() ManySortedSet of the carrier of S
for t being Term of S,V
for o being OperSymbol of S st t . {} = [o,the carrier of S] holds
ex a being ArgumentSeq of Sym o,V st t = [o,the carrier of S] -tree a
let V be V16() ManySortedSet of the carrier of S; :: thesis: for t being Term of S,V
for o being OperSymbol of S st t . {} = [o,the carrier of S] holds
ex a being ArgumentSeq of Sym o,V st t = [o,the carrier of S] -tree a
let t be Term of S,V; :: thesis: for o being OperSymbol of S st t . {} = [o,the carrier of S] holds
ex a being ArgumentSeq of Sym o,V st t = [o,the carrier of S] -tree a
let o be OperSymbol of S; :: thesis: ( t . {} = [o,the carrier of S] implies ex a being ArgumentSeq of Sym o,V st t = [o,the carrier of S] -tree a )
assume A1: t . {} = [o,the carrier of S] ; :: thesis: ex a being ArgumentSeq of Sym o,V st t = [o,the carrier of S] -tree a
set X = V;
set G = DTConMSA V;
reconsider t = t as Element of TS (DTConMSA V) ;
[o,the carrier of S] = Sym o,V by MSAFREE:def 11;
then consider p being FinSequence of TS (DTConMSA V) such that
A2: t = (Sym o,V) -tree p and
A3: Sym o,V ==> roots p by A1, DTCONSTR:10;
reconsider a = p as FinSequence of S -Terms V ;
a is SubtreeSeq of Sym o,V by A3, DTCONSTR:def 9;
then reconsider a = a as ArgumentSeq of Sym o,V by Def2;
take a ; :: thesis: t = [o,the carrier of S] -tree a
thus t = [o,the carrier of S] -tree a by A2, MSAFREE:def 11; :: thesis: verum