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 ) ) )
assume A1: 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 ) )
A2: Args o,U1 = product (the Sorts of U1 * (the_arity_of o)) by PRALG_2:10;
then A3: dom x = dom (the Sorts of U1 * (the_arity_of o)) by A1, CARD_3:18;
dom the Sorts of U1 = the carrier of S by PARTFUN1:def 4;
then rng (the_arity_of o) c= dom the Sorts of U1 by FINSEQ_1:def 4;
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 A1, A2, A3, CARD_3:18, RELAT_1:46; :: thesis: verum