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: len (h2 * (h1 * a)) = len (h1 * a) by Th1;
A2: dom (h2 * (h1 * a)) = dom (h1 * a) by Th1;
A3: len (h1 * a) = len a by Th1;
A4: dom (h1 * a) = dom a by Th1;
A5: len a = len ((h2 * h1) * a) by Th1;
A7: ( dom a = Seg (len a) & dom (h2 * (h1 * a)) = Seg (len a) & dom (h1 * a) = Seg (len a) & dom ((h2 * h1) * a) = Seg (len a) ) by A2, A4, A5, FINSEQ_1:def 3;

now

let n be Nat; :: thesis: ( n in dom (h2 * (h1 * a)) implies (h2 * (h1 * a)) . n = ((h2 * h1) * a) . n )
assume A8: 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 Th1
.= h2 . (h1 . (a . n)) by A8, Th1, A2
.= (h2 * h1) . (a . n) by A8, FINSEQ_2:13, FUNCT_2:21, A7
.= ((h2 * h1) * a) . n by A8, Th1, A7 ;
:: thesis: verum

end;

hence h2 * (h1 * a) = (h2 * h1) * a by A1, A3, A5, FINSEQ_2:10; :: thesis: verum