let U1, U2, U3 be Universal_Algebra; 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; 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; for a being FinSequence of U1 holds h2 * (h1 * a) = (h2 * h1) * a
let a be FinSequence of U1; 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 for n being Nat st n in dom (h2 * (h1 * a)) holds
(h2 * (h1 * a)) . n = ((h2 * h1) * a) . nend;
( 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; verum