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