let S be non empty non void ManySortedSign ; :: thesis: for A being MSAlgebra of 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 of 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:10;
then A1: ex f being Function st
( x = f & dom f = dom (the Sorts of A * (the_arity_of o)) & ( for y being set 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 4; :: 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 8;
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:23; :: thesis: verum