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 4;
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:46;
x in Args o,(product A) ;
then x in product (the Sorts of (product A) * (the_arity_of o)) by PRALG_2:10;
then x . n in ((SORTS A) * (the_arity_of o)) . n by A2, CARD_3:18;
then x . n in (SORTS A) . ((the_arity_of o) . n) by A2, FUNCT_1:22;
then x . n in (SORTS A) . ((the_arity_of o) /. n) by A1, PARTFUN1:def 8;
hence x . n in product (Carrier A,((the_arity_of o) /. n)) by PRALG_2:def 17; :: thesis: verum