let S be non empty non void ManySortedSign ; :: thesis: for A being MSAlgebra over S
for o being OperSymbol of S
for a being Function st a in Args (o,A) holds
( dom a = dom (the_arity_of o) & ( for i being set st i in dom (the_arity_of o) holds
a . i in the Sorts of A . ((the_arity_of o) /. i) ) )
let A be MSAlgebra over S; :: thesis: for o being OperSymbol of S
for a being Function st a in Args (o,A) holds
( dom a = dom (the_arity_of o) & ( for i being set st i in dom (the_arity_of o) holds
a . i in the Sorts of A . ((the_arity_of o) /. i) ) )
let o be OperSymbol of S; :: thesis: for a being Function st a in Args (o,A) holds
( dom a = dom (the_arity_of o) & ( for i being set st i in dom (the_arity_of o) holds
a . i in the Sorts of A . ((the_arity_of o) /. i) ) )
let x be Function; :: thesis: ( x in Args (o,A) implies ( dom x = dom (the_arity_of o) & ( for i being set st i in dom (the_arity_of o) holds
x . i in the Sorts of A . ((the_arity_of o) /. i) ) ) )
assume x in Args (o,A) ; :: thesis: ( dom x = dom (the_arity_of o) & ( for i being set st i in dom (the_arity_of o) holds
x . i in the Sorts of A . ((the_arity_of o) /. i) ) )
then x in product ( the Sorts of A * (the_arity_of o)) by PRALG_2:3;
then A1: ex f being Function st
( x = f & dom f = dom ( the Sorts of A * (the_arity_of o)) & ( for y being object st y in dom ( the Sorts of A * (the_arity_of o)) holds
f . y in ( the Sorts of A * (the_arity_of o)) . y ) ) by CARD_3:def 5;
hence A2: dom x = dom (the_arity_of o) by PARTFUN1:def 2; :: thesis: for i being set st i in dom (the_arity_of o) holds
x . i in the Sorts of A . ((the_arity_of o) /. i)
let y be set ; :: thesis: ( y in dom (the_arity_of o) implies x . y in the Sorts of A . ((the_arity_of o) /. y) )
assume A3: y in dom (the_arity_of o) ; :: thesis: x . y in the Sorts of A . ((the_arity_of o) /. y)
then A4: (the_arity_of o) . y = (the_arity_of o) /. y by PARTFUN1:def 6;
x . y in ( the Sorts of A * (the_arity_of o)) . y by A1, A2, A3;
hence x . y in the Sorts of A . ((the_arity_of o) /. y) by A3, A4, FUNCT_1:13; :: thesis: verum