let S be OrderSortedSign; :: thesis:
let X be V16() 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 9;
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 9;
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 9; :: thesis: