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 () & ( for y being set st y in dom ( the Sorts of U1 * ()) holds
x . y in ( the Sorts of U1 * ()) . 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 () & ( for y being set st y in dom ( the Sorts of U1 * ()) holds
x . y in ( the Sorts of U1 * ()) . y ) )

let U1 be MSAlgebra over S; :: thesis: for x being Function st x in Args (o,U1) holds
( dom x = dom () & ( for y being set st y in dom ( the Sorts of U1 * ()) holds
x . y in ( the Sorts of U1 * ()) . y ) )

let x be Function; :: thesis: ( x in Args (o,U1) implies ( dom x = dom () & ( for y being set st y in dom ( the Sorts of U1 * ()) holds
x . y in ( the Sorts of U1 * ()) . y ) ) )

A1: Args (o,U1) = product ( the Sorts of U1 * ()) by PRALG_2:3;
dom the Sorts of U1 = the carrier of S by PARTFUN1:def 2;
then A2: rng () c= dom the Sorts of U1 by FINSEQ_1:def 4;
assume A3: x in Args (o,U1) ; :: thesis: ( dom x = dom () & ( for y being set st y in dom ( the Sorts of U1 * ()) holds
x . y in ( the Sorts of U1 * ()) . y ) )

then dom x = dom ( the Sorts of U1 * ()) by ;
hence ( dom x = dom () & ( for y being set st y in dom ( the Sorts of U1 * ()) holds
x . y in ( the Sorts of U1 * ()) . y ) ) by ; :: thesis: verum