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