ex v being Vector of V ex a being Scalar of R st
( v <> 0. V & f . v = a * v ) by A1, Def1;
hence ex b₁ being Element of R ex v being Vector of V st
( v <> 0. V & f . v = b₁ * v ) ; :: thesis: verum