deffunc H₁( Element of X) -> Element of the carrier of X = Sum ($1 ExpSeq );
consider f being Function of the carrier of X,the carrier of X such that
A1: for z being Element of X holds f . z = H₁(z) from FUNCT_2:sch 4();
thus 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 ) by A1; :: thesis: verum