let S be non empty non void ManySortedSign ; :: thesis: for A being MSAlgebra of 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 of 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

A3: dom (the Sorts of A * (the_arity_of o)) = dom (the_arity_of o) by PRALG_2:10;
A4: Args o,A = product (the Sorts of A * (the_arity_of o)) by PRALG_2:10;
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:23;
(the_arity_of o) /. i = (the_arity_of o) . i by A2, A6, PARTFUN1:def 8;
then f . i in the Sorts of A . ((the_arity_of o) /. i) by A1, A2, A6, A4, A3, A9, CARD_3:18;
hence c . i = ((h2 ** h1) . ((the_arity_of o) /. i)) . (f . i) by A5, A7, A8, FUNCT_2:21; :: thesis: verum

end;

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