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 ArgumentSeq of Sym o,V holds
( len a = len (the_arity_of o) & 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 & t = a /. i & the_sort_of t = (the_arity_of o) . i & the_sort_of t = (the_arity_of o) /. i ) ) )
let V be V16() ManySortedSet of the carrier of S; :: thesis: for o being OperSymbol of S
for a being ArgumentSeq of Sym o,V holds
( len a = len (the_arity_of o) & 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 & t = a /. i & the_sort_of t = (the_arity_of o) . i & the_sort_of t = (the_arity_of o) /. i ) ) )
let o be OperSymbol of S; :: thesis: for a being ArgumentSeq of Sym o,V holds
( len a = len (the_arity_of o) & 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 & t = a /. i & the_sort_of t = (the_arity_of o) . i & the_sort_of t = (the_arity_of o) /. i ) ) )
let a be ArgumentSeq of Sym o,V; :: thesis: ( len a = len (the_arity_of o) & 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 & t = a /. i & the_sort_of t = (the_arity_of o) . i & the_sort_of t = (the_arity_of o) /. i ) ) )
set X = V;
reconsider p = a as FinSequence of TS (DTConMSA V) by Def1;
Sym o,V ==> roots a by Th21;
then A1: p in (((FreeSort V) # ) * the Arity of S) . o by MSAFREE:10;
then A2: dom p = dom (the_arity_of o) by MSAFREE:9;
hence ( len a = len (the_arity_of o) & dom a = dom (the_arity_of o) ) by FINSEQ_3:31; :: thesis: for i being Nat st i in dom a holds
ex t being Term of S,V st
( t = a . i & t = a /. i & the_sort_of t = (the_arity_of o) . i & the_sort_of t = (the_arity_of o) /. i )
let i be Nat; :: thesis: ( i in dom a implies ex t being Term of S,V st
( t = a . i & t = a /. i & the_sort_of t = (the_arity_of o) . i & the_sort_of t = (the_arity_of o) /. i ) )
reconsider t = a /. i as Term of S,V ;
assume A3: i in dom a ; :: thesis: ex t being Term of S,V st
( t = a . i & t = a /. i & the_sort_of t = (the_arity_of o) . i & the_sort_of t = (the_arity_of o) /. i )
then A4: i <= len a by FINSEQ_3:27;
take t ; :: thesis: ( t = a . i & t = a /. i & the_sort_of t = (the_arity_of o) . i & the_sort_of t = (the_arity_of o) /. i )
1 <= i by A3, FINSEQ_3:27;
hence t = a . i by A4, FINSEQ_4:24; :: thesis: ( t = a /. i & the_sort_of t = (the_arity_of o) . i & the_sort_of t = (the_arity_of o) /. i )
then t in FreeSort V,((the_arity_of o) /. i) by A1, A3, MSAFREE:9;
then the_sort_of t = (the_arity_of o) /. i by Def5;
hence ( t = a /. i & the_sort_of t = (the_arity_of o) . i & the_sort_of t = (the_arity_of o) /. i ) by A2, A3, PARTFUN1:def 8; :: thesis: verum