take 1 ; :: according to ALGSEQ_1:def 1 :: thesis: for b₁ being set holds
( not 1 <= b₁ or (1_. L) . b₁ = 0. L )
let i be Nat; :: thesis: ( not 1 <= i or (1_. L) . i = 0. L )
A1: i in NAT by ORDINAL1:def 12;
assume i >= 1 ; :: thesis: (1_. L) . i = 0. L
hence (1_. L) . i = (0_. L) . i by FUNCT_7:32
.= 0. L by A1, FUNCOP_1:7 ;
:: thesis: verum