let a be Variable; :: thesis: a . 1 = 0
a in VAR ;
then consider k being Element of NAT such that
A1: a = <*0,k*> ;
thus a . 1 = 0 by A1, FINSEQ_1:44; :: thesis: verum