let S be non empty non void ManySortedSign ; for V being V2() 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 V2() 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 t be 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 o be OperSymbol of S; ( 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]
; 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
; t = [o, the carrier of S] -tree a
thus
t = [o, the carrier of S] -tree a
by A2, MSAFREE:def 9; verum