let n be Nat; :: thesis: for L being non empty ZeroStr
for x being Element of L holds n + 1 is_at_least_length_of seq (n,x)
let L be non empty ZeroStr ; :: thesis: for x being Element of L holds n + 1 is_at_least_length_of seq (n,x)
let x be Element of L; :: thesis: n + 1 is_at_least_length_of seq (n,x)
let i be Nat; :: according to ALGSEQ_1:def 2 :: thesis: ( not n + 1 <= i or (seq (n,x)) . i = 0. L )
assume A1: i >= n + 1 ; :: thesis: (seq (n,x)) . i = 0. L
n + 0 < n + 1 by XREAL_1:8;
hence (seq (n,x)) . i = (0_. L) . i by A1, FUNCT_7:32
.= 0. L by ORDINAL1:def 12, FUNCOP_1:7 ;
:: thesis: verum