let S be non empty non void ManySortedSign ; :: thesis: for A being MSAlgebra of 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 of 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:10;
then 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 x is Function ; :: thesis: verum