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