let I be non empty set ; for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for x being Element of Args (o,(product A))
for n being set st n in dom (the_arity_of o) holds
x . n in product (Carrier (A,((the_arity_of o) /. n)))
let S be non empty non void ManySortedSign ; for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for x being Element of Args (o,(product A))
for n being set st n in dom (the_arity_of o) holds
x . n in product (Carrier (A,((the_arity_of o) /. n)))
let A be MSAlgebra-Family of I,S; for o being OperSymbol of S
for x being Element of Args (o,(product A))
for n being set st n in dom (the_arity_of o) holds
x . n in product (Carrier (A,((the_arity_of o) /. n)))
let o be OperSymbol of S; for x being Element of Args (o,(product A))
for n being set st n in dom (the_arity_of o) holds
x . n in product (Carrier (A,((the_arity_of o) /. n)))
let x be Element of Args (o,(product A)); for n being set st n in dom (the_arity_of o) holds
x . n in product (Carrier (A,((the_arity_of o) /. n)))
let n be set ; ( n in dom (the_arity_of o) implies x . n in product (Carrier (A,((the_arity_of o) /. n))) )
assume A1:
n in dom (the_arity_of o)
; x . n in product (Carrier (A,((the_arity_of o) /. n)))
dom (SORTS A) = the carrier of S
by PARTFUN1:def 2;
then
rng (the_arity_of o) c= dom (SORTS A)
;
then A2:
n in dom ((SORTS A) * (the_arity_of o))
by A1, RELAT_1:27;
x in Args (o,(product A))
;
then
x in product ( the Sorts of (product A) * (the_arity_of o))
by PRALG_2:3;
then
x . n in ((SORTS A) * (the_arity_of o)) . n
by A2, CARD_3:9;
then
x . n in (SORTS A) . ((the_arity_of o) . n)
by A2, FUNCT_1:12;
then
x . n in (SORTS A) . ((the_arity_of o) /. n)
by A1, PARTFUN1:def 6;
hence
x . n in product (Carrier (A,((the_arity_of o) /. n)))
by PRALG_2:def 10; verum