let S be non empty non void ManySortedSign ; :: thesis: for V being V5() ManySortedSet of
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
a . i is Term of S,V ) )
let V be V5() ManySortedSet of ; :: 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
a . i is Term of S,V ) )
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
a . i is Term of S,V ) )
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
a . i is Term of S,V ) )
thus ( len a = len (the_arity_of o) & dom a = dom (the_arity_of o) ) by Lm8; :: thesis: for i being Nat st i in dom a holds
a . i is Term of S,V
let i be Nat; :: thesis: ( i in dom a implies a . i is Term of S,V )
assume i in dom a ; :: thesis: a . i is Term of S,V
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 a . i is Term of S,V ; :: thesis: verum