let S be non empty non void ManySortedSign ; for A being MSAlgebra over S
for h1, h2 being ManySortedFunction of A,A
for o being OperSymbol of S
for a being Element of Args (o,A) st a in Args (o,A) holds
h2 # (h1 # a) = (h2 ** h1) # a
let A be MSAlgebra over S; for h1, h2 being ManySortedFunction of A,A
for o being OperSymbol of S
for a being Element of Args (o,A) st a in Args (o,A) holds
h2 # (h1 # a) = (h2 ** h1) # a
let h1, h2 be ManySortedFunction of A,A; for o being OperSymbol of S
for a being Element of Args (o,A) st a in Args (o,A) holds
h2 # (h1 # a) = (h2 ** h1) # a
set h = h2 ** h1;
let o be OperSymbol of S; for a being Element of Args (o,A) st a in Args (o,A) holds
h2 # (h1 # a) = (h2 ** h1) # a
let a be Element of Args (o,A); ( a in Args (o,A) implies h2 # (h1 # a) = (h2 ** h1) # a )
assume A1:
a in Args (o,A)
; h2 # (h1 # a) = (h2 ** h1) # a
then reconsider f = a, b = h1 # a, c = h2 # (h1 # a) as Function by Th1;
A2:
dom f = dom (the_arity_of o)
by A1, Th2;
now for i being Nat st i in dom f holds
c . i = ((h2 ** h1) . ((the_arity_of o) /. i)) . (f . i)A3:
dom ( the Sorts of A * (the_arity_of o)) = dom (the_arity_of o)
by PRALG_2:3;
A4:
Args (
o,
A)
= product ( the Sorts of A * (the_arity_of o))
by PRALG_2:3;
let i be
Nat;
( i in dom f implies c . i = ((h2 ** h1) . ((the_arity_of o) /. i)) . (f . i) )reconsider f1 =
h1 . ((the_arity_of o) /. i),
f2 =
h2 . ((the_arity_of o) /. i) as
Function of
( the Sorts of A . ((the_arity_of o) /. i)),
( the Sorts of A . ((the_arity_of o) /. i)) ;
A5:
(h2 ** h1) . ((the_arity_of o) /. i) = f2 * f1
by MSUALG_3:2;
assume A6:
i in dom f
;
c . i = ((h2 ** h1) . ((the_arity_of o) /. i)) . (f . i)then A7:
f1 . (f . i) = b . i
by A1, MSUALG_3:24;
dom b = dom (the_arity_of o)
by A1, Th2;
then A8:
f2 . (b . i) = c . i
by A1, A2, A6, MSUALG_3:24;
A9:
the
Sorts of
A . ((the_arity_of o) . i) = ( the Sorts of A * (the_arity_of o)) . i
by A2, A6, FUNCT_1:13;
(the_arity_of o) /. i = (the_arity_of o) . i
by A2, A6, PARTFUN1:def 6;
then
f . i in the
Sorts of
A . ((the_arity_of o) /. i)
by A1, A2, A6, A4, A3, A9, CARD_3:9;
hence
c . i = ((h2 ** h1) . ((the_arity_of o) /. i)) . (f . i)
by A5, A7, A8, FUNCT_2:15;
verum end;
hence
h2 # (h1 # a) = (h2 ** h1) # a
by A1, MSUALG_3:24; verum