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 (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 over 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:29;

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 2;

then A4: dom p = dom ( the Sorts of A * (the_arity_of o)) by A3, RELAT_1:27;

then (( the Sorts of A #) * the Arity of S) . o = ( the Sorts of A #) . (the_arity_of o) by FUNCT_1:13

.= product ( the Sorts of A * (the_arity_of o)) by FINSEQ_2:def 5 ;

hence p in Args (o,A) by A4, A5, CARD_3:def 5; :: thesis: verum

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 over 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:29;

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 2;

then A4: dom p = dom ( the Sorts of A * (the_arity_of o)) by A3, RELAT_1:27;

A5: now :: thesis: for x being object st x in dom ( the Sorts of A * (the_arity_of o)) holds

p . x in ( the Sorts of A * (the_arity_of o)) . x

dom the Arity of S = the carrier' of S
by FUNCT_2:def 1;p . x in ( the Sorts of A * (the_arity_of o)) . x

let x be object ; :: 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 ;

( the Sorts of A * (the_arity_of o)) . k = the Sorts of A . ((the_arity_of o) . k) by A6, FUNCT_1:12

.= the Sorts of A . ((the_arity_of o) /. k) by A3, A4, A6, PARTFUN1:def 6 ;

hence p . x in ( the Sorts of A * (the_arity_of o)) . x by A2, A4, A6; :: thesis: verum

end;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 ;

( the Sorts of A * (the_arity_of o)) . k = the Sorts of A . ((the_arity_of o) . k) by A6, FUNCT_1:12

.= the Sorts of A . ((the_arity_of o) /. k) by A3, A4, A6, PARTFUN1:def 6 ;

hence p . x in ( the Sorts of A * (the_arity_of o)) . x by A2, A4, A6; :: thesis: verum

then (( the Sorts of A #) * the Arity of S) . o = ( the Sorts of A #) . (the_arity_of o) by FUNCT_1:13

.= product ( the Sorts of A * (the_arity_of o)) by FINSEQ_2:def 5 ;

hence p in Args (o,A) by A4, A5, CARD_3:def 5; :: thesis: verum