deffunc H₁( Element of V1) -> Element of the carrier of V2 = Sum (lmlt ((Line (((LineVec2Mx ($1 |-- b1)) * M),1)),B2));
consider f being Function of V1,V2 such that
A1: for x being Element of V1 holds f . x = H₁(x) from FUNCT_2:sch 4();
take f ; :: thesis: for v being Vector of V1 holds f . v = Sum (lmlt ((Line (((LineVec2Mx (v |-- b1)) * M),1)),B2))
thus for v being Vector of V1 holds f . v = Sum (lmlt ((Line (((LineVec2Mx (v |-- b1)) * M),1)),B2)) by A1; :: thesis: verum