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