deffunc H_{1}( Element of X) -> Element of the carrier of X = Sum ($1 ExpSeq);

ex f being Function of the carrier of X, the carrier of X st

for z being Element of X holds f . z = H_{1}(z)
from FUNCT_2:sch 4();

hence ex b_{1} being Function of the carrier of X, the carrier of X st

for z being Element of X holds b_{1} . z = Sum (z ExpSeq)
; :: thesis: verum

ex f being Function of the carrier of X, the carrier of X st

for z being Element of X holds f . z = H

hence ex b

for z being Element of X holds b