take
0
; :: according to ALGSEQ_1:def 1 :: thesis: for b_{1} being set holds

( not 0 <= b_{1} or (0_. L) . b_{1} = 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

( not 0 <= b

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