deffunc H_{1}( 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_{1}(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_{1} being Function of ([#] (OrderedFIN I)), the carrier of L st

for j being Element of Fin I holds b_{1} . j = Sum (x,j)
; :: thesis: verum

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

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

for j being Element of Fin I holds b