let S be non empty non void ManySortedSign ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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); :: thesis: ( a in Args (o,A) implies h2 # (h1 # a) = (h2 ** h1) # a )
assume A1: a in Args (o,A) ; :: thesis: 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 :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

end;

hence h2 # (h1 # a) = (h2 ** h1) # a by A1, MSUALG_3:24; :: thesis: verum