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 of S -Terms V holds
( a is ArgumentSeq of Sym (o,V) iff Sym (o,V) ==> roots a )
let V be non-empty 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 6;
hence ( a is ArgumentSeq of Sym (o,V) iff Sym (o,V) ==> roots a ) by Def2; :: thesis: verum