let S be non empty non void ManySortedSign ; :: thesis: for V being V2() ManySortedSet of the carrier of S
for o being OperSymbol of S
for a being FinSequence of S -Terms V 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
for t being Term of S,V st t = a . i holds
the_sort_of t = (the_arity_of o) . i or for i being Nat st i in dom a holds
for t being Term of S,V st t = a . i holds
the_sort_of t = (the_arity_of o) /. i ) holds
a is ArgumentSeq of Sym (o,V)
let V be V2() ManySortedSet of the carrier of S; :: thesis: for o being OperSymbol of S
for a being FinSequence of S -Terms V 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
for t being Term of S,V st t = a . i holds
the_sort_of t = (the_arity_of o) . i or for i being Nat st i in dom a holds
for t being Term of S,V st t = a . i holds
the_sort_of t = (the_arity_of o) /. i ) holds
a is ArgumentSeq of Sym (o,V)
let o be OperSymbol of S; :: thesis: for a being FinSequence of S -Terms V 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
for t being Term of S,V st t = a . i holds
the_sort_of t = (the_arity_of o) . i or for i being Nat st i in dom a holds
for t being Term of S,V st t = a . i holds
the_sort_of t = (the_arity_of o) /. i ) holds
a is ArgumentSeq of Sym (o,V)
let a be FinSequence of S -Terms V; :: 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
for t being Term of S,V st t = a . i holds
the_sort_of t = (the_arity_of o) . i or for i being Nat st i in dom a holds
for t being Term of S,V st t = a . i holds
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
for t being Term of S,V st t = a . i holds
the_sort_of t = (the_arity_of o) . i or for i being Nat st i in dom a holds
for t being Term of S,V st t = a . i holds
the_sort_of t = (the_arity_of o) /. i ) ; :: thesis: a is ArgumentSeq of Sym (o,V)
A3: now :: thesis: for i being Nat st i in dom a holds
a . i in S -Terms V
let i be Nat; :: thesis: ( i in dom a implies a . i in S -Terms V )
assume i in dom a ; :: thesis: a . i in S -Terms V
then A4: a . i in rng a by FUNCT_1:def 3;
rng a c= S -Terms V by FINSEQ_1:def 4;
hence a . i in S -Terms V by A4; :: thesis: verum
end;
now :: thesis: ( ( ( for i being Nat st i in dom a holds
for t being Term of S,V st t = a . i holds
the_sort_of t = (the_arity_of o) . i ) & ( 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
for t being Term of S,V st t = a . i holds
the_sort_of t = (the_arity_of o) /. i ) & ( 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 ) ) ) )
per cases ( for i being Nat st i in dom a holds
for t being Term of S,V st t = a . i holds
the_sort_of t = (the_arity_of o) . i or for i being Nat st i in dom a holds
for t being Term of S,V st t = a . i holds
the_sort_of t = (the_arity_of o) /. i ) by A2;
case A5: for i being Nat st i in dom a holds
for t being Term of S,V st t = a . i holds
the_sort_of t = (the_arity_of o) . i ; :: thesis: 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 )
let i be Nat; :: thesis: ( i in dom a implies ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) . i ) )
assume A6: i in dom a ; :: thesis: ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) . i )
then reconsider t = a . i as Term of S,V by A3;
take t = t; :: thesis: ( t = a . i & the_sort_of t = (the_arity_of o) . i )
thus ( t = a . i & the_sort_of t = (the_arity_of o) . i ) by A5, A6; :: thesis: verum
end;
case A7: for i being Nat st i in dom a holds
for t being Term of S,V st t = a . i holds
the_sort_of t = (the_arity_of o) /. i ; :: thesis: 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 )
let i be Nat; :: thesis: ( i in dom a implies ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) /. i ) )
assume A8: i in dom a ; :: thesis: ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) /. i )
then reconsider t = a . i as Term of S,V by A3;
take t = t; :: thesis: ( t = a . i & the_sort_of t = (the_arity_of o) /. i )
thus ( t = a . i & the_sort_of t = (the_arity_of o) /. i ) by A7, A8; :: thesis: verum
end;
end;
end;
hence a is ArgumentSeq of Sym (o,V) by A1, Th24; :: thesis: verum