let S be non empty non void ManySortedSign ; :: thesis: for o being OperSymbol of S
for V being V5 ManySortedSet of the carrier of S
for x being set holds
( x is ArgumentSeq of Sym o,V iff x is Element of Args o,(FreeMSA V) )
let o be OperSymbol of S; :: thesis: for V being V5 ManySortedSet of the carrier of S
for x being set holds
( x is ArgumentSeq of Sym o,V iff x is Element of Args o,(FreeMSA V) )
let V be V5 ManySortedSet of the carrier of S; :: thesis: for x being set holds
( x is ArgumentSeq of Sym o,V iff x is Element of Args o,(FreeMSA V) )
A1: FreeMSA V = MSAlgebra(# (FreeSort V),(FreeOper V) #) by MSAFREE:def 16;
let x be set ; :: thesis: ( x is ArgumentSeq of Sym o,V iff x is Element of Args o,(FreeMSA V) )

hereby :: thesis: ( x is Element of Args o,(FreeMSA V) implies x is ArgumentSeq of Sym o,V )

assume x is ArgumentSeq of Sym o,V ; :: thesis: x is Element of Args o,(FreeMSA V)
then reconsider p = x as ArgumentSeq of Sym o,V ;
reconsider p = p as FinSequence of TS (DTConMSA V) by MSATERM:def 1;
Sym o,V ==> roots p by MSATERM:21;
hence x is Element of Args o,(FreeMSA V) by A1, MSAFREE:10; :: thesis: verum

end;

assume x is Element of Args o,(FreeMSA V) ; :: thesis: x is ArgumentSeq of Sym o,V
then reconsider x = x as Element of Args o,(FreeMSA V) ;
rng x c= TS (DTConMSA V)

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng x or y in TS (DTConMSA V) )
assume y in rng x ; :: thesis: y in TS (DTConMSA V)
then consider z being set such that
A2: ( z in dom x & y = x . z ) by FUNCT_1:def 5;
reconsider z = z as Element of NAT by A2;
dom x = dom (the_arity_of o) by MSUALG_6:2;
then ( y in (FreeSort V) . ((the_arity_of o) /. z) & (FreeSort V) . ((the_arity_of o) /. z) = FreeSort V,((the_arity_of o) /. z) & FreeSort V,((the_arity_of o) /. z) c= S -Terms V ) by A1, A2, MSAFREE:def 13, MSATERM:12, MSUALG_6:2;
hence y in TS (DTConMSA V) ; :: thesis: verum

end;

then reconsider x = x as FinSequence of TS (DTConMSA V) by FINSEQ_1:def 4;
( Sym o,V ==> roots x & TS (DTConMSA V) = S -Terms V ) by A1, MSAFREE:10, MSATERM:def 1;
hence x is ArgumentSeq of Sym o,V by MSATERM:21; :: thesis: verum