let S be OrderSortedSign; :: thesis:
let X be V5() ManySortedSet of ; :: 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;
A3: x in (((ParsedTerms X) # ) * the Arity of S) . o by A1, MSUALG_1:def 9;
thus x is FinSequence of TS (DTConOSA X) by A2, Th5; :: thesis:
reconsider x1 = x as FinSequence of TS (DTConOSA X) by A3, Th5;
OSSym o,X ==> roots x1 by A2, Th7;
hence OSSym o,X ==> roots x ; :: thesis:

end;

assume A4: ( x is FinSequence of TS (DTConOSA X) & OSSym o,X ==> roots x ) ; :: thesis:
then reconsider x1 = x as FinSequence of TS (DTConOSA X) ;
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: