deffunc H₁( Element of Fin I) -> Element of L = Sum (x,$1);
consider f being Function of (Fin I), the carrier of L such that
A1: for t being Element of Fin I holds f . t = H₁(t) from FUNCT_2:sch 4();
the carrier of (OrderedFIN I) = Fin I by YELLOW_1:1;
then A2: [#] (OrderedFIN I) = Fin I by STRUCT_0:def 3;
reconsider f = f as Function of ([#] (OrderedFIN I)), the carrier of L by A2;
for j being Element of Fin I holds f . j = Sum (x,j) by A1;
hence ex b₁ being Function of ([#] (OrderedFIN I)), the carrier of L st
for j being Element of Fin I holds b₁ . j = Sum (x,j) ; :: thesis: verum