let U1, U2, U3 be Universal_Algebra; :: thesis: for h1 being Function of U1,U2
for h2 being Function of U2,U3
for a being FinSequence of U1 holds h2 * (h1 * a) = (h2 * h1) * a
let h1 be Function of U1,U2; :: thesis: for h2 being Function of U2,U3
for a being FinSequence of U1 holds h2 * (h1 * a) = (h2 * h1) * a
let h2 be Function of U2,U3; :: thesis: for a being FinSequence of U1 holds h2 * (h1 * a) = (h2 * h1) * a
let a be FinSequence of U1; :: thesis: h2 * (h1 * a) = (h2 * h1) * a
A1: dom a = Seg (len a) by FINSEQ_1:def 3;
A2: dom (h2 * (h1 * a)) = dom (h1 * a) by FINSEQ_3:120;
dom (h1 * a) = dom a by FINSEQ_3:120;
then A3: dom (h2 * (h1 * a)) = Seg (len a) by A2, FINSEQ_1:def 3;
A4: len a = len ((h2 * h1) * a) by FINSEQ_3:120;
then A5: dom ((h2 * h1) * a) = Seg (len a) by FINSEQ_1:def 3;

A6: now :: thesis: for n being Nat st n in dom (h2 * (h1 * a)) holds
(h2 * (h1 * a)) . n = ((h2 * h1) * a) . n

let n be Nat; :: thesis: ( n in dom (h2 * (h1 * a)) implies (h2 * (h1 * a)) . n = ((h2 * h1) * a) . n )
assume A7: n in dom (h2 * (h1 * a)) ; :: thesis: (h2 * (h1 * a)) . n = ((h2 * h1) * a) . n
hence (h2 * (h1 * a)) . n = h2 . ((h1 * a) . n) by FINSEQ_3:120
.= h2 . (h1 . (a . n)) by A2, A7, FINSEQ_3:120
.= (h2 * h1) . (a . n) by A1, A3, A7, FINSEQ_2:11, FUNCT_2:15
.= ((h2 * h1) * a) . n by A3, A5, A7, FINSEQ_3:120 ;
:: thesis: verum

end;

( len (h2 * (h1 * a)) = len (h1 * a) & len (h1 * a) = len a ) by FINSEQ_3:120;
hence h2 * (h1 * a) = (h2 * h1) * a by A4, A6, FINSEQ_2:9; :: thesis: verum