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

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