let S be non empty non void ManySortedSign ; :: thesis: for o being OperSymbol of S
for U1 being MSAlgebra of 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 of 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 of 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:10;
dom the Sorts of U1 = the carrier of S by PARTFUN1:def 4;
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:18;
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:18, RELAT_1:46; :: thesis: verum