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)
for i being Nat st i in dom a holds
for t being Term of S,V st t = a . i holds
( 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)
for i being Nat st i in dom a holds
for t being Term of S,V st t = a . i holds
( 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)
for i being Nat st i in dom a holds
for t being Term of S,V st t = a . i holds
( 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: for i being Nat st i in dom a holds
for t being Term of S,V st t = a . i holds
( 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 for t being Term of S,V st t = a . i holds
( t = a /. i & the_sort_of t = (the_arity_of o) . i & the_sort_of t = (the_arity_of o) /. i ) )
assume i in dom a ; :: thesis: for t being Term of S,V st t = a . i holds
( t = a /. i & the_sort_of t = (the_arity_of o) . i & the_sort_of t = (the_arity_of o) /. i )
then 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 ) by Lm8;
hence for t being Term of S,V st t = a . i holds
( t = a /. i & the_sort_of t = (the_arity_of o) . i & the_sort_of t = (the_arity_of o) /. i ) ; :: thesis: verum