let n be Nat; :: thesis: for L being non empty ZeroStr
for x being Element of L st x <> 0. L holds
len (seq (n,x)) = n + 1
let L be non empty ZeroStr ; :: thesis: for x being Element of L st x <> 0. L holds
len (seq (n,x)) = n + 1
let x be Element of L; :: thesis: ( x <> 0. L implies len (seq (n,x)) = n + 1 )
assume A1: x <> 0. L ; :: thesis: len (seq (n,x)) = n + 1
set p = seq (n,x);
for m being Nat st m is_at_least_length_of seq (n,x) holds
n + 1 <= m
proof
let m be Nat; :: thesis: ( m is_at_least_length_of seq (n,x) implies n + 1 <= m )
assume A2: m is_at_least_length_of seq (n,x) ; :: thesis: n + 1 <= m
(seq (n,x)) . n = x by Th24;
hence n + 1 <= m by A1, A2, NAT_1:13; :: thesis: verum
end;
hence len (seq (n,x)) = n + 1 by Th26, ALGSEQ_1:def 3; :: thesis: verum