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)
for n being set st n in dom (the_arity_of o) holds
(F # x) . n = (F . ((the_arity_of o) /. n)) . (x . n)
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)
for n being set st n in dom (the_arity_of o) holds
(F # x) . n = (F . ((the_arity_of o) /. n)) . (x . n)
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)
for n being set st n in dom (the_arity_of o) holds
(F # x) . n = (F . ((the_arity_of o) /. n)) . (x . n)
let F be ManySortedFunction of U1,U2; :: thesis: for x being Element of Args (o,U1)
for n being set st n in dom (the_arity_of o) holds
(F # x) . n = (F . ((the_arity_of o) /. n)) . (x . n)
let x be Element of Args (o,U1); :: thesis: for n being set st n in dom (the_arity_of o) holds
(F # x) . n = (F . ((the_arity_of o) /. n)) . (x . n)
let n be set ; :: thesis: ( n in dom (the_arity_of o) implies (F # x) . n = (F . ((the_arity_of o) /. n)) . (x . n) )
assume A1: n in dom (the_arity_of o) ; :: thesis: (F # x) . n = (F . ((the_arity_of o) /. n)) . (x . n)
dom F = the carrier of S by PARTFUN1:def 2;
then a1: rng (the_arity_of o) c= dom F ;
then A2: n in dom (F * (the_arity_of o)) by A1, RELAT_1:27;
B2: dom x = dom (the_arity_of o) by MSUALG_6:2;
dom (F * (the_arity_of o)) = dom (the_arity_of o) by a1, RELAT_1:27;
then dom ((F * (the_arity_of o)) .. x) = (dom (the_arity_of o)) /\ (dom x) by PRALG_1:def 19
.= dom (the_arity_of o) by B2 ;
then a2: n in dom ((F * (the_arity_of o)) .. x) by A1;
A3: x in product (doms (F * (the_arity_of o))) by Th12;
thus (F # x) . n = ((Frege (F * (the_arity_of o))) . x) . n by MSUALG_3:def 5
.= ((F * (the_arity_of o)) .. x) . n by A3, PRALG_2:def 2
.= ((F * (the_arity_of o)) . n) . (x . n) by a2, PRALG_1:def 19
.= (F . ((the_arity_of o) . n)) . (x . n) by A2, FUNCT_1:12
.= (F . ((the_arity_of o) /. n)) . (x . n) by A1, PARTFUN1:def 6 ; :: thesis: verum