let I be non empty set ; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: 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)); :: thesis: 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 ; :: thesis: ( 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) ; :: thesis: 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; :: thesis: verum