let k, l be Nat; :: thesis: for R being non empty ZeroStr
for p being AlgSequence of R st k is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds
k <= m ) & l is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds
l <= m ) holds
k = l
let R be non empty ZeroStr ; :: thesis: for p being AlgSequence of R st k is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds
k <= m ) & l is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds
l <= m ) holds
k = l
let p be AlgSequence of R; :: thesis: ( k is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds
k <= m ) & l is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds
l <= m ) implies k = l )
assume ( k is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds
k <= m ) & l is_at_least_length_of p & ( for m being Nat st m is_at_least_length_of p holds
l <= m ) ) ; :: thesis: k = l
then ( k <= l & l <= k ) ;
hence k = l by XXREAL_0:1; :: thesis: verum