let S be non empty non void ManySortedSign ; :: thesis: for V being V5() ManySortedSet of the carrier of S
for o being OperSymbol of S
for a being FinSequence of S -Terms V holds
( a is ArgumentSeq of Sym o,V iff Sym o,V ==> roots a )
let V be V5() ManySortedSet of the carrier of S; :: thesis: for o being OperSymbol of S
for a being FinSequence of S -Terms V holds
( a is ArgumentSeq of Sym o,V iff Sym o,V ==> roots a )
let o be OperSymbol of S; :: thesis: for a being FinSequence of S -Terms V holds
( a is ArgumentSeq of Sym o,V iff Sym o,V ==> roots a )
let a be FinSequence of S -Terms V; :: thesis: ( a is ArgumentSeq of Sym o,V iff Sym o,V ==> roots a )
( a is SubtreeSeq of Sym o,V iff Sym o,V ==> roots a ) by DTCONSTR:def 9;
hence ( a is ArgumentSeq of Sym o,V iff Sym o,V ==> roots a ) by Def2; :: thesis: verum