let S be non empty non void ManySortedSign ; :: thesis: for A being MSAlgebra of S
for o being OperSymbol of S
for p being FinSequence st len p = len (the_arity_of o) & ( for k being Nat st k in dom p holds
p . k in the Sorts of A . ((the_arity_of o) /. k) ) holds
p in Args o,A
let A be MSAlgebra of S; :: thesis: for o being OperSymbol of S
for p being FinSequence st len p = len (the_arity_of o) & ( for k being Nat st k in dom p holds
p . k in the Sorts of A . ((the_arity_of o) /. k) ) holds
p in Args o,A
let o be OperSymbol of S; :: thesis: for p being FinSequence st len p = len (the_arity_of o) & ( for k being Nat st k in dom p holds
p . k in the Sorts of A . ((the_arity_of o) /. k) ) holds
p in Args o,A
let p be FinSequence; :: thesis: ( len p = len (the_arity_of o) & ( for k being Nat st k in dom p holds
p . k in the Sorts of A . ((the_arity_of o) /. k) ) implies p in Args o,A )
assume that
A1: len p = len (the_arity_of o) and
A2: for k being Nat st k in dom p holds
p . k in the Sorts of A . ((the_arity_of o) /. k) ; :: thesis: p in Args o,A
set D = the Sorts of A * (the_arity_of o);
A3: dom p = dom (the_arity_of o) by A1, FINSEQ_3:31;
rng (the_arity_of o) c= the carrier of S ;
then rng (the_arity_of o) c= dom the Sorts of A by PARTFUN1:def 4;
then A4: dom p = dom (the Sorts of A * (the_arity_of o)) by A3, RELAT_1:46;

A5: now

let x be set ; :: thesis: ( x in dom (the Sorts of A * (the_arity_of o)) implies p . x in (the Sorts of A * (the_arity_of o)) . x )
assume A6: x in dom (the Sorts of A * (the_arity_of o)) ; :: thesis: p . x in (the Sorts of A * (the_arity_of o)) . x
then reconsider k = x as Nat by A4;
(the Sorts of A * (the_arity_of o)) . k = the Sorts of A . ((the_arity_of o) . k) by A6, FUNCT_1:22
.= the Sorts of A . ((the_arity_of o) /. k) by A3, A4, A6, PARTFUN1:def 8 ;
hence p . x in (the Sorts of A * (the_arity_of o)) . x by A2, A4, A6; :: thesis: verum

end;

dom the Arity of S = the carrier' of S by FUNCT_2:def 1;
then ((the Sorts of A # ) * the Arity of S) . o = (the Sorts of A # ) . (the_arity_of o) by FUNCT_1:23
.= product (the Sorts of A * (the_arity_of o)) by PBOOLE:def 19 ;
hence p in Args o,A by A4, A5, CARD_3:def 5; :: thesis: verum