let S be non empty non void ManySortedSign ; :: thesis: for A being MSAlgebra over S
for o being OperSymbol of S
for a being set st a in Args (o,A) holds
a is Function
let A be MSAlgebra over S; :: thesis: for o being OperSymbol of S
for a being set st a in Args (o,A) holds
a is Function
let o be OperSymbol of S; :: thesis: for a being set st a in Args (o,A) holds
a is Function
let x be set ; :: thesis: ( x in Args (o,A) implies x is Function )
assume x in Args (o,A) ; :: thesis: x is Function
then x in product ( the Sorts of A * (the_arity_of o)) by PRALG_2:3;
then 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 x is Function ; :: thesis: verum