let S be non empty non void ManySortedSign ; :: thesis: for o being OperSymbol of S
for U1, U2 being non-empty MSAlgebra over 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 over 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 over 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:3;
A2: dom x = dom (the_arity_of o) by MSUALG_6:2;
dom F = the carrier of S by PARTFUN1:def 2;
then A3: rng (the_arity_of o) c= dom F ;
A4: now :: thesis: for n being object st n in dom (doms (F * (the_arity_of o))) holds
n in dom x
let n be object ; :: 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 dom (F * (the_arity_of o)) by FUNCT_6:def 2;
then n in dom (F * (the_arity_of o)) ;
hence n in dom x by A3, A2, RELAT_1:27; :: thesis: verum
end;
A5: dom x = dom ( the Sorts of U1 * (the_arity_of o)) by A1, CARD_3:9;
A6: now :: thesis: for n being object st n in dom (doms (F * (the_arity_of o))) holds
x . n in (doms (F * (the_arity_of o))) . n
let n be object ; :: 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 3;
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:27;
then (F * (the_arity_of o)) . n = F . s1 by FUNCT_1:12;
then A10: (doms (F * (the_arity_of o))) . n = dom (F . s1) by A9, FUNCT_6:22
.= 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:9;
hence x . n in (doms (F * (the_arity_of o))) . n by A5, A4, A7, A10, FUNCT_1:12; :: thesis: verum
end;
now :: thesis: for n being object st n in dom x holds
n in dom (doms (F * (the_arity_of o)))
let n be object ; :: 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:27;
n in dom (F * (the_arity_of o)) by A11;
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))) ;
dom (doms (F * (the_arity_of o))) c= dom x by A4;
then dom x = dom (doms (F * (the_arity_of o))) by A12;
hence x in product (doms (F * (the_arity_of o))) by A6, CARD_3:9; :: thesis: verum