let R be comRing; :: thesis: for f being Element of the carrier of (Polynom-Ring R)
for i being Nat st i >= 1 & i is_at_least_length_of f & f . (i - 1) <> 0. R holds
len f = i
let f be Element of the carrier of (Polynom-Ring R); :: thesis: for i being Nat st i >= 1 & i is_at_least_length_of f & f . (i - 1) <> 0. R holds
len f = i
for i being Nat st i >= 1 & i is_at_least_length_of f & f . (i - 1) <> 0. R holds
len f = i

proof

let i be Nat; :: thesis: ( i >= 1 & i is_at_least_length_of f & f . (i - 1) <> 0. R implies len f = i )
assume A1: ( i >= 1 & i is_at_least_length_of f & f . (i - 1) <> 0. R ) ; :: thesis: len f = i
then A2: len f <= i by ALGSEQ_1:def 3;
for n, m being Nat st n - 1 < m & m <= n holds
n = m

proof

let n, m be Nat; :: thesis: ( n - 1 < m & m <= n implies n = m )
assume A4: ( n - 1 < m & m <= n ) ; :: thesis: n = m
then (n - 1) + 1 < m + 1 by XREAL_1:8;
then n <= m by NAT_1:13;
hence n = m by A4, XXREAL_0:1; :: thesis: verum

end;

hence len f = i by A2, A1, ALGSEQ_1:8; :: thesis: verum

end;

hence for i being Nat st i >= 1 & i is_at_least_length_of f & f . (i - 1) <> 0. R holds
len f = i ; :: thesis: verum