let S be non empty non void ManySortedSign ; :: thesis: for V being non-empty 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 non-empty 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 9;
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 6;
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 9; :: thesis: verum