ex f being Function of Q,Q st
for u being Element of Q holds f . u = H₁(u) from FUNCT_2:sch 4();
hence ex b₁ being Function of Q,Q st
for u being Element of Q holds b₁ . u = L_map (u,x,y) ; :: thesis: verum