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,(FreeMSA V)) )

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,(FreeMSA V)) )

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,(FreeMSA V)) )

let x be set ; :: thesis: ( x is ArgumentSeq of Sym (o,V) iff x is Element of Args (o,(FreeMSA V)) )

A1: TS (DTConMSA V) = S -Terms V by MSATERM:def 1;

A2: FreeMSA V = MSAlgebra(# (FreeSort V),(FreeOper V) #) by MSAFREE:def 14;

then reconsider x = x as Element of Args (o,(FreeMSA V)) ;

rng x c= TS (DTConMSA V)

Sym (o,V) ==> roots x by A2, MSAFREE:10;

hence x is ArgumentSeq of Sym (o,V) by A1, MSATERM:21; :: thesis: verum

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,(FreeMSA V)) )

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,(FreeMSA V)) )

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,(FreeMSA V)) )

let x be set ; :: thesis: ( x is ArgumentSeq of Sym (o,V) iff x is Element of Args (o,(FreeMSA V)) )

A1: TS (DTConMSA V) = S -Terms V by MSATERM:def 1;

A2: FreeMSA V = MSAlgebra(# (FreeSort V),(FreeOper V) #) by MSAFREE:def 14;

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

assume
x is Element of Args (o,(FreeMSA V))
; :: thesis: 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 A2, MSAFREE:10; :: thesis: verum

end;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 A2, MSAFREE:10; :: thesis: verum

then reconsider x = x as Element of Args (o,(FreeMSA V)) ;

rng x c= TS (DTConMSA V)

proof

then reconsider x = x as FinSequence of TS (DTConMSA V) by FINSEQ_1:def 4;
let y be object ; :: 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 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) . ((the_arity_of o) /. z) = FreeSort (V,((the_arity_of o) /. z)) by MSAFREE:def 11;

dom x = dom (the_arity_of o) by MSUALG_6:2;

then y in (FreeSort V) . ((the_arity_of o) /. z) by A2, A3, A4, MSUALG_6:2;

hence y in TS (DTConMSA V) by A5; :: thesis: verum

end;assume y in rng x ; :: thesis: y in TS (DTConMSA V)

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) . ((the_arity_of o) /. z) = FreeSort (V,((the_arity_of o) /. z)) by MSAFREE:def 11;

dom x = dom (the_arity_of o) by MSUALG_6:2;

then y in (FreeSort V) . ((the_arity_of o) /. z) by A2, A3, A4, MSUALG_6:2;

hence y in TS (DTConMSA V) by A5; :: thesis: verum

Sym (o,V) ==> roots x by A2, MSAFREE:10;

hence x is ArgumentSeq of Sym (o,V) by A1, MSATERM:21; :: thesis: verum