let S be non empty non void ManySortedSign ; :: thesis: for V being V16() ManySortedSet of the carrier of S
for o being OperSymbol of S
for a being FinSequence st ( len a = len (the_arity_of o) or dom a = dom (the_arity_of o) ) & ( for i being Nat st i in dom a holds
ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) . i ) or for i being Nat st i in dom a holds
ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) /. i ) ) holds
a is ArgumentSeq of Sym o,V
let V be V16() ManySortedSet of the carrier of S; :: thesis: for o being OperSymbol of S
for a being FinSequence st ( len a = len (the_arity_of o) or dom a = dom (the_arity_of o) ) & ( for i being Nat st i in dom a holds
ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) . i ) or for i being Nat st i in dom a holds
ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) /. i ) ) holds
a is ArgumentSeq of Sym o,V
set X = V;
let o be OperSymbol of S; :: thesis: for a being FinSequence st ( len a = len (the_arity_of o) or dom a = dom (the_arity_of o) ) & ( for i being Nat st i in dom a holds
ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) . i ) or for i being Nat st i in dom a holds
ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) /. i ) ) holds
a is ArgumentSeq of Sym o,V
let a be FinSequence; :: thesis: ( ( len a = len (the_arity_of o) or dom a = dom (the_arity_of o) ) & ( for i being Nat st i in dom a holds
ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) . i ) or for i being Nat st i in dom a holds
ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) /. i ) ) implies a is ArgumentSeq of Sym o,V )
assume that
A1: ( len a = len (the_arity_of o) or dom a = dom (the_arity_of o) ) and
A2: ( for i being Nat st i in dom a holds
ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) . i ) or for i being Nat st i in dom a holds
ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) /. i ) ) ; :: thesis: a is ArgumentSeq of Sym o,V
rng a c= TS (DTConMSA V)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng a or x in TS (DTConMSA V) )
assume x in rng a ; :: thesis: x in TS (DTConMSA V)
then consider i being set such that
A3: i in dom a and
A4: x = a . i by FUNCT_1:def 5;
reconsider i = i as Nat by A3;
( ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) . i ) or ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) /. i ) ) by A2, A3;
hence x in TS (DTConMSA V) by A4; :: thesis: verum

end;

then reconsider p = a as FinSequence of TS (DTConMSA V) by FINSEQ_1:def 4;
A5: dom a = dom (the_arity_of o) by A1, FINSEQ_3:31;

now

let n be Nat; :: thesis: ( n in dom p implies p . n in FreeSort V,((the_arity_of o) /. n) )
assume A6: n in dom p ; :: thesis: p . n in FreeSort V,((the_arity_of o) /. n)
thus p . n in FreeSort V,((the_arity_of o) /. n) :: thesis: verum

proof

per cases ( ex t being Term of S,V st
( t = a . n & the_sort_of t = (the_arity_of o) . n ) or ex t being Term of S,V st
( t = a . n & the_sort_of t = (the_arity_of o) /. n ) ) by A2, A6;

suppose ex t being Term of S,V st
( t = a . n & the_sort_of t = (the_arity_of o) . n ) ; :: thesis: p . n in FreeSort V,((the_arity_of o) /. n)

then consider t being Term of S,V such that
A7: t = a . n and
A8: the_sort_of t = (the_arity_of o) . n ;
the_sort_of t = (the_arity_of o) /. n by A5, A6, A8, PARTFUN1:def 8;
hence p . n in FreeSort V,((the_arity_of o) /. n) by A7, Def5; :: thesis: verum

end;

suppose ex t being Term of S,V st
( t = a . n & the_sort_of t = (the_arity_of o) /. n ) ; :: thesis: p . n in FreeSort V,((the_arity_of o) /. n)

hence p . n in FreeSort V,((the_arity_of o) /. n) by Def5; :: thesis: verum

end;

end;

end;

end;

then p in (((FreeSort V) # ) * the Arity of S) . o by A5, MSAFREE:9;
then A9: Sym o,V ==> roots p by MSAFREE:10;
S -Terms V = TS (DTConMSA V) ;
hence a is ArgumentSeq of Sym o,V by A9, Th21; :: thesis: verum