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

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

( not 1 <= b

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