let S be non empty non void ManySortedSign ; :: thesis: for V being non-empty ManySortedSet of the carrier of S
for o being OperSymbol of S
for a being FinSequence holds
( ( [o, the carrier of S] -tree a in S -Terms V & a is DTree-yielding ) iff a is ArgumentSeq of Sym (o,V) )
let V be non-empty ManySortedSet of the carrier of S; :: thesis: for o being OperSymbol of S
for a being FinSequence holds
( ( [o, the carrier of S] -tree a in S -Terms V & a is DTree-yielding ) iff a is ArgumentSeq of Sym (o,V) )
let o be OperSymbol of S; :: thesis: for a being FinSequence holds
( ( [o, the carrier of S] -tree a in S -Terms V & a is DTree-yielding ) iff a is ArgumentSeq of Sym (o,V) )
let a be FinSequence; :: thesis: ( ( [o, the carrier of S] -tree a in S -Terms V & a is DTree-yielding ) iff a is ArgumentSeq of Sym (o,V) )
A1: [o, the carrier of S] = Sym (o,V) by MSAFREE:def 9;
A2: S -Terms V = TS (DTConMSA V) ;

hereby :: thesis: ( a is ArgumentSeq of Sym (o,V) implies ( [o, the carrier of S] -tree a in S -Terms V & a is DTree-yielding ) )

assume [o, the carrier of S] -tree a in S -Terms V ; :: thesis: ( a is DTree-yielding implies a is ArgumentSeq of Sym (o,V) )
then reconsider t = [o, the carrier of S] -tree a as Element of TS (DTConMSA V) ;
assume A3: a is DTree-yielding ; :: thesis: a is ArgumentSeq of Sym (o,V)
then t . {} = [o, the carrier of S] by TREES_4:def 4;
then consider p being FinSequence of TS (DTConMSA V) such that
A4: t = (Sym (o,V)) -tree p and
A5: Sym (o,V) ==> roots p by A1, DTCONSTR:10;
a = p by A3, A4, TREES_4:15;
then a is SubtreeSeq of Sym (o,V) by A5, DTCONSTR:def 6;
hence a is ArgumentSeq of Sym (o,V) by A2, Def2; :: thesis: verum

end;

assume a is ArgumentSeq of Sym (o,V) ; :: thesis: ( [o, the carrier of S] -tree a in S -Terms V & a is DTree-yielding )
then reconsider a = a as ArgumentSeq of Sym (o,V) ;
reconsider p = a as FinSequence of TS (DTConMSA V) by Def1;
p is SubtreeSeq of Sym (o,V) by Def2;
then Sym (o,V) ==> roots p by DTCONSTR:def 6;
hence ( [o, the carrier of S] -tree a in S -Terms V & a is DTree-yielding ) by A1, DTCONSTR:def 1; :: thesis: verum