let S be non empty non void ManySortedSign ; :: thesis: for A being MSAlgebra over S
for o being OperSymbol of S
for p being FinSequence st len p = len () & ( for k being Nat st k in dom p holds
p . k in the Sorts of A . (() /. k) ) holds
p in Args (o,A)

let A be MSAlgebra over S; :: thesis: for o being OperSymbol of S
for p being FinSequence st len p = len () & ( for k being Nat st k in dom p holds
p . k in the Sorts of A . (() /. k) ) holds
p in Args (o,A)

let o be OperSymbol of S; :: thesis: for p being FinSequence st len p = len () & ( for k being Nat st k in dom p holds
p . k in the Sorts of A . (() /. k) ) holds
p in Args (o,A)

let p be FinSequence; :: thesis: ( len p = len () & ( for k being Nat st k in dom p holds
p . k in the Sorts of A . (() /. k) ) implies p in Args (o,A) )

assume that
A1: len p = len () and
A2: for k being Nat st k in dom p holds
p . k in the Sorts of A . (() /. k) ; :: thesis: p in Args (o,A)
set D = the Sorts of A * ();
A3: dom p = dom () by ;
rng () c= the carrier of S ;
then rng () c= dom the Sorts of A by PARTFUN1:def 2;
then A4: dom p = dom ( the Sorts of A * ()) by ;
A5: now :: thesis: for x being object st x in dom ( the Sorts of A * ()) holds
p . x in ( the Sorts of A * ()) . x
let x be object ; :: thesis: ( x in dom ( the Sorts of A * ()) implies p . x in ( the Sorts of A * ()) . x )
assume A6: x in dom ( the Sorts of A * ()) ; :: thesis: p . x in ( the Sorts of A * ()) . x
then reconsider k = x as Nat ;
( the Sorts of A * ()) . k = the Sorts of A . (() . k) by
.= the Sorts of A . (() /. k) by ;
hence p . x in ( the Sorts of A * ()) . 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 #) . () by FUNCT_1:13
.= product ( the Sorts of A * ()) by FINSEQ_2:def 5 ;
hence p in Args (o,A) by ; :: thesis: verum