let S be non empty non void ManySortedSign ; :: thesis: for o being OperSymbol of S
for V being V2() 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,()) )

let o be OperSymbol of S; :: thesis: for V being V2() 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,()) )

let V be V2() 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,()) )

let x be set ; :: thesis: ( x is ArgumentSeq of Sym (o,V) iff x is Element of Args (o,()) )
A1: TS () = S -Terms V by MSATERM:def 1;
A2: FreeMSA V = MSAlgebra(# (),() #) by MSAFREE:def 14;
hereby :: thesis: ( x is Element of Args (o,()) implies x is ArgumentSeq of Sym (o,V) )
assume x is ArgumentSeq of Sym (o,V) ; :: thesis: x is Element of Args (o,())
then reconsider p = x as ArgumentSeq of Sym (o,V) ;
reconsider p = p as FinSequence of TS () by MSATERM:def 1;
Sym (o,V) ==> roots p by MSATERM:21;
hence x is Element of Args (o,()) by ; :: thesis: verum
end;
assume x is Element of Args (o,()) ; :: thesis: x is ArgumentSeq of Sym (o,V)
then reconsider x = x as Element of Args (o,()) ;
rng x c= TS ()
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng x or y in TS () )
assume y in rng x ; :: thesis: y in TS ()
then consider z being object such that
A3: z in dom x and
A4: y = x . z by FUNCT_1:def 3;
reconsider z = z as Element of NAT by A3;
A5: (FreeSort V) . (() /. z) = FreeSort (V,(() /. z)) by MSAFREE:def 11;
dom x = dom () by MSUALG_6:2;
then y in () . (() /. z) by ;
hence y in TS () by A5; :: thesis: verum
end;
then reconsider x = x as FinSequence of TS () by FINSEQ_1:def 4;
Sym (o,V) ==> roots x by ;
hence x is ArgumentSeq of Sym (o,V) by ; :: thesis: verum