let S be non empty non void ManySortedSign ; :: thesis: for o being OperSymbol of S
for U1 being MSAlgebra over S
for x being Function st x in Args (o,U1) holds
( dom x = dom (the_arity_of o) & ( for y being set st y in dom ( the Sorts of U1 * (the_arity_of o)) holds
x . y in ( the Sorts of U1 * (the_arity_of o)) . y ) )
let o be OperSymbol of S; :: thesis: for U1 being MSAlgebra over S
for x being Function st x in Args (o,U1) holds
( dom x = dom (the_arity_of o) & ( for y being set st y in dom ( the Sorts of U1 * (the_arity_of o)) holds
x . y in ( the Sorts of U1 * (the_arity_of o)) . y ) )
let U1 be MSAlgebra over S; :: thesis: for x being Function st x in Args (o,U1) holds
( dom x = dom (the_arity_of o) & ( for y being set st y in dom ( the Sorts of U1 * (the_arity_of o)) holds
x . y in ( the Sorts of U1 * (the_arity_of o)) . y ) )
let x be Function; :: thesis: ( x in Args (o,U1) implies ( dom x = dom (the_arity_of o) & ( for y being set st y in dom ( the Sorts of U1 * (the_arity_of o)) holds
x . y in ( the Sorts of U1 * (the_arity_of o)) . y ) ) )
A1: Args (o,U1) = product ( the Sorts of U1 * (the_arity_of o)) by PRALG_2:3;
dom the Sorts of U1 = the carrier of S by PARTFUN1:def 2;
then A2: rng (the_arity_of o) c= dom the Sorts of U1 by FINSEQ_1:def 4;
assume A3: x in Args (o,U1) ; :: thesis: ( dom x = dom (the_arity_of o) & ( for y being set st y in dom ( the Sorts of U1 * (the_arity_of o)) holds
x . y in ( the Sorts of U1 * (the_arity_of o)) . y ) )
then dom x = dom ( the Sorts of U1 * (the_arity_of o)) by A1, CARD_3:9;
hence ( dom x = dom (the_arity_of o) & ( for y being set st y in dom ( the Sorts of U1 * (the_arity_of o)) holds
x . y in ( the Sorts of U1 * (the_arity_of o)) . y ) ) by A3, A1, A2, CARD_3:9, RELAT_1:27; :: thesis: verum