let S be non empty non void ManySortedSign ; :: thesis: for o being OperSymbol of S
for U1, U2 being non-empty MSAlgebra of S
for F being ManySortedFunction of U1,U2
for x being Element of Args o,U1 holds x in product (doms (F * (the_arity_of o)))
let o be OperSymbol of S; :: thesis: for U1, U2 being non-empty MSAlgebra of S
for F being ManySortedFunction of U1,U2
for x being Element of Args o,U1 holds x in product (doms (F * (the_arity_of o)))
let U1, U2 be non-empty MSAlgebra of S; :: thesis: for F being ManySortedFunction of U1,U2
for x being Element of Args o,U1 holds x in product (doms (F * (the_arity_of o)))
let F be ManySortedFunction of U1,U2; :: thesis: for x being Element of Args o,U1 holds x in product (doms (F * (the_arity_of o)))
let x be Element of Args o,U1; :: thesis: x in product (doms (F * (the_arity_of o)))
x in Args o,U1 ;
then A1: x in product (the Sorts of U1 * (the_arity_of o)) by PRALG_2:10;
then A2: dom x = dom (the Sorts of U1 * (the_arity_of o)) by CARD_3:18
.= dom (the_arity_of o) by PRALG_2:10 ;
dom F = the carrier of S by PARTFUN1:def 4;
then A3: rng (the_arity_of o) c= dom F ;

A4: now

let n be set ; :: thesis: ( n in dom (doms (F * (the_arity_of o))) implies n in dom x )
assume n in dom (doms (F * (the_arity_of o))) ; :: thesis: n in dom x
then n in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) by FUNCT_6:def 2;
then n in dom (F * (the_arity_of o)) by FUNCT_6:28;
hence n in dom x by A3, A2, RELAT_1:46; :: thesis: verum

end;

A5: dom x = dom (the Sorts of U1 * (the_arity_of o)) by A1, CARD_3:18;

A6: now

let n be set ; :: thesis: ( n in dom (doms (F * (the_arity_of o))) implies x . n in (doms (F * (the_arity_of o))) . n )
assume A7: n in dom (doms (F * (the_arity_of o))) ; :: thesis: x . n in (doms (F * (the_arity_of o))) . n
then A8: n in dom (the_arity_of o) by A2, A4;
then (the_arity_of o) . n in rng (the_arity_of o) by FUNCT_1:def 5;
then reconsider s1 = (the_arity_of o) . n as Element of the carrier of S ;
A9: n in dom (F * (the_arity_of o)) by A3, A8, RELAT_1:46;
then (F * (the_arity_of o)) . n = F . s1 by FUNCT_1:22;
then A10: (doms (F * (the_arity_of o))) . n = dom (F . s1) by A9, FUNCT_6:31
.= the Sorts of U1 . s1 by FUNCT_2:def 1 ;
n in dom (the Sorts of U1 * (the_arity_of o)) by A5, A4, A7;
then x . n in (the Sorts of U1 * (the_arity_of o)) . n by A1, CARD_3:18;
hence x . n in (doms (F * (the_arity_of o))) . n by A5, A4, A7, A10, FUNCT_1:22; :: thesis: verum

end;

now

let n be set ; :: thesis: ( n in dom x implies n in dom (doms (F * (the_arity_of o))) )
assume n in dom x ; :: thesis: n in dom (doms (F * (the_arity_of o)))
then A11: n in dom (F * (the_arity_of o)) by A3, A2, RELAT_1:46;
(F * (the_arity_of o)) . n is Function ;
then n in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) by A11, FUNCT_6:28;
hence n in dom (doms (F * (the_arity_of o))) by FUNCT_6:def 2; :: thesis: verum

end;

then A12: dom x c= dom (doms (F * (the_arity_of o))) by TARSKI:def 3;
dom (doms (F * (the_arity_of o))) c= dom x by A4, TARSKI:def 3;
then dom x = dom (doms (F * (the_arity_of o))) by A12, XBOOLE_0:def 10;
hence x in product (doms (F * (the_arity_of o))) by A6, CARD_3:18; :: thesis: verum