let S be non empty non void ManySortedSign ; :: thesis: for o being OperSymbol of S
for U1, U2, U3 being non-empty MSAlgebra of S
for H1 being ManySortedFunction of U1,U2
for H2 being ManySortedFunction of U2,U3
for x being Element of Args o,U1 holds (H2 ** H1) # x = H2 # (H1 # x)
let o be OperSymbol of S; :: thesis: for U1, U2, U3 being non-empty MSAlgebra of S
for H1 being ManySortedFunction of U1,U2
for H2 being ManySortedFunction of U2,U3
for x being Element of Args o,U1 holds (H2 ** H1) # x = H2 # (H1 # x)
let U1, U2, U3 be non-empty MSAlgebra of S; :: thesis: for H1 being ManySortedFunction of U1,U2
for H2 being ManySortedFunction of U2,U3
for x being Element of Args o,U1 holds (H2 ** H1) # x = H2 # (H1 # x)
let H1 be ManySortedFunction of U1,U2; :: thesis: for H2 being ManySortedFunction of U2,U3
for x being Element of Args o,U1 holds (H2 ** H1) # x = H2 # (H1 # x)
let H2 be ManySortedFunction of U2,U3; :: thesis: for x being Element of Args o,U1 holds (H2 ** H1) # x = H2 # (H1 # x)
let x be Element of Args o,U1; :: thesis: (H2 ** H1) # x = H2 # (H1 # x)
A1: dom x = dom (the_arity_of o) by Th6;
A2: dom (H1 # x) = dom (the_arity_of o) by Th6;
A3: for y being set st y in dom (the_arity_of o) holds
((H2 ** H1) # x) . y = (H2 # (H1 # x)) . y

proof

rng (the_arity_of o) c= the carrier of S by FINSEQ_1:def 4;
then rng (the_arity_of o) c= dom the Sorts of U1 by PARTFUN1:def 4;
then A4: dom (the Sorts of U1 * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:46;
let y be set ; :: thesis: ( y in dom (the_arity_of o) implies ((H2 ** H1) # x) . y = (H2 # (H1 # x)) . y )
assume A5: y in dom (the_arity_of o) ; :: thesis: ((H2 ** H1) # x) . y = (H2 # (H1 # x)) . y
then reconsider n = y as Nat ;
set F = H2 ** H1;
set p = (the_arity_of o) /. n;
A6: ((H2 ** H1) # x) . n = ((H2 ** H1) . ((the_arity_of o) /. n)) . (x . n) by A1, A5, Def8;
(the_arity_of o) /. n = (the_arity_of o) . n by A5, PARTFUN1:def 8;
then A7: (the Sorts of U1 * (the_arity_of o)) . n = the Sorts of U1 . ((the_arity_of o) /. n) by A5, A4, FUNCT_1:22;
A8: (H2 ** H1) . ((the_arity_of o) /. n) = (H2 . ((the_arity_of o) /. n)) * (H1 . ((the_arity_of o) /. n)) by Th2;
A9: dom (H1 . ((the_arity_of o) /. n)) = the Sorts of U1 . ((the_arity_of o) /. n) by FUNCT_2:def 1;
then dom ((H2 . ((the_arity_of o) /. n)) * (H1 . ((the_arity_of o) /. n))) = dom (H1 . ((the_arity_of o) /. n)) by FUNCT_2:def 1;
hence ((H2 ** H1) # x) . y = (H2 . ((the_arity_of o) /. n)) . ((H1 . ((the_arity_of o) /. n)) . (x . n)) by A5, A6, A4, A9, A7, A8, Th6, FUNCT_1:22
.= (H2 . ((the_arity_of o) /. n)) . ((H1 # x) . n) by A1, A5, Def8
.= (H2 # (H1 # x)) . y by A2, A5, Def8 ;
:: thesis: verum

end;

( dom ((H2 ** H1) # x) = dom (the_arity_of o) & dom (H2 # (H1 # x)) = dom (the_arity_of o) ) by Th6;
hence (H2 ** H1) # x = H2 # (H1 # x) by A3, FUNCT_1:9; :: thesis: verum