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
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 of 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 of 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)
A2: x in product (doms (F * (the_arity_of o))) by Th13;
dom F = the carrier of S by PARTFUN1:def 4;
then rng (the_arity_of o) c= dom F ;
then A3: n in dom (F * (the_arity_of o)) by A1, RELAT_1:46;
thus (F # x) . n = ((Frege (F * (the_arity_of o))) . x) . n by MSUALG_3:def 7
.= ((F * (the_arity_of o)) .. x) . n by A2, PRALG_2:def 8
.= ((F * (the_arity_of o)) . n) . (x . n) by A3, PRALG_1:def 17
.= (F . ((the_arity_of o) . n)) . (x . n) by A3, FUNCT_1:22
.= (F . ((the_arity_of o) /. n)) . (x . n) by A1, PARTFUN1:def 8 ; :: thesis: verum