consider a being Vector of V such that
A2: a <> 0. V by A1;
take <:a:> ; :: thesis: ex a being Vector of V st
( a <> 0. V & <:a:> = <:a:> )
thus ex a being Vector of V st
( a <> 0. V & <:a:> = <:a:> ) by A2; :: thesis: verum