let S be OrderSortedSign; for X being V2() ManySortedSet of S
for o being OperSymbol of S
for x being FinSequence holds
( x in Args (o,(ParsedTermsOSA X)) iff ( x is FinSequence of TS (DTConOSA X) & OSSym (o,X) ==> roots x ) )
let X be V2() ManySortedSet of S; for o being OperSymbol of S
for x being FinSequence holds
( x in Args (o,(ParsedTermsOSA X)) iff ( x is FinSequence of TS (DTConOSA X) & OSSym (o,X) ==> roots x ) )
let o be OperSymbol of S; for x being FinSequence holds
( x in Args (o,(ParsedTermsOSA X)) iff ( x is FinSequence of TS (DTConOSA X) & OSSym (o,X) ==> roots x ) )
let x be FinSequence; ( x in Args (o,(ParsedTermsOSA X)) iff ( x is FinSequence of TS (DTConOSA X) & OSSym (o,X) ==> roots x ) )
set PTA = ParsedTermsOSA X;
assume that
A3:
x is FinSequence of TS (DTConOSA X)
and
A4:
OSSym (o,X) ==> roots x
; x in Args (o,(ParsedTermsOSA X))
reconsider x1 = x as FinSequence of TS (DTConOSA X) by A3;
x1 in (((ParsedTerms X) #) * the Arity of S) . o
by A4, Th7;
hence
x in Args (o,(ParsedTermsOSA X))
by MSUALG_1:def 4; verum