let S be non empty non void ManySortedSign ; :: thesis: for V being non-empty 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 non-empty 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:29; :: 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:25;
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:25;
hence t = a . i by A4, FINSEQ_4:15; :: 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 6; :: thesis: verum