let S be OrderSortedSign; :: thesis:
let X be non-empty ManySortedSet of S; :: thesis:
let o be OperSymbol of S; :: thesis:
let x be FinSequence; :: thesis:
set PTA = ParsedTermsOSA X;

hereby :: thesis:

assume A1: x in Args (o,(ParsedTermsOSA X)) ; :: thesis:
then A2: x in (( the Sorts of (ParsedTermsOSA X) #) * the Arity of S) . o by MSUALG_1:def 4;
hence x is FinSequence of TS (DTConOSA X) by Th5; :: thesis:
x in (((ParsedTerms X) #) * the Arity of S) . o by A1, MSUALG_1:def 4;
then reconsider x1 = x as FinSequence of TS (DTConOSA X) by Th5;
OSSym (o,X) ==> roots x1 by A2, Th7;
hence OSSym (o,X) ==> roots x ; :: thesis:

end;

assume that
A3: x is FinSequence of TS (DTConOSA X) and
A4: OSSym (o,X) ==> roots x ; :: thesis:
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; :: thesis: