deffunc H₁( 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₁(z) from FUNCT_2:sch 4();
hence ex b₁ being Function of the carrier of X,the carrier of X st
for z being Element of X holds b₁ . z = Sum (z ExpSeq ) ; :: thesis: verum