let S be non empty non void ManySortedSign ; :: thesis: for o being OperSymbol of S
for U1, U2, U3 being non-empty MSAlgebra over 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 over 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 over 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 () by Th6;
A2: dom (H1 # x) = dom () by Th6;
A3: for y being object st y in dom () holds
((H2 ** H1) # x) . y = (H2 # (H1 # x)) . y
proof
rng () c= the carrier of S by FINSEQ_1:def 4;
then rng () c= dom the Sorts of U1 by PARTFUN1:def 2;
then A4: dom ( the Sorts of U1 * ()) = dom () by RELAT_1:27;
let y be object ; :: thesis: ( y in dom () implies ((H2 ** H1) # x) . y = (H2 # (H1 # x)) . y )
assume A5: y in dom () ; :: thesis: ((H2 ** H1) # x) . y = (H2 # (H1 # x)) . y
then reconsider n = y as Nat ;
set F = H2 ** H1;
set p = () /. n;
A6: ((H2 ** H1) # x) . n = ((H2 ** H1) . (() /. n)) . (x . n) by A1, A5, Def6;
(the_arity_of o) /. n = () . n by ;
then A7: ( the Sorts of U1 * ()) . n = the Sorts of U1 . (() /. n) by ;
A8: (H2 ** H1) . (() /. n) = (H2 . (() /. n)) * (H1 . (() /. n)) by Th2;
A9: dom (H1 . (() /. n)) = the Sorts of U1 . (() /. n) by FUNCT_2:def 1;
then dom ((H2 . (() /. n)) * (H1 . (() /. n))) = dom (H1 . (() /. n)) by FUNCT_2:def 1;
hence ((H2 ** H1) # x) . y = (H2 . (() /. n)) . ((H1 . (() /. n)) . (x . n)) by A5, A6, A4, A9, A7, A8, Th6, FUNCT_1:12
.= (H2 . (() /. n)) . ((H1 # x) . n) by A1, A5, Def6
.= (H2 # (H1 # x)) . y by A2, A5, Def6 ;
:: thesis: verum
end;
( dom ((H2 ** H1) # x) = dom () & dom (H2 # (H1 # x)) = dom () ) by Th6;
hence (H2 ** H1) # x = H2 # (H1 # x) by ; :: thesis: verum