let R be non empty ZeroStr ; :: thesis: for p being AlgSequence of R ex k being Element of NAT st
( k is_at_least_length_of p & ( for n being Nat st n is_at_least_length_of p holds
k <= n ) )
let p be AlgSequence of R; :: thesis: ex k being Element of NAT st
( k is_at_least_length_of p & ( for n being Nat st n is_at_least_length_of p holds
k <= n ) )
defpred S₁[ Nat] means $1 is_at_least_length_of p;
A1: ex m being Nat st S₁[m] by Lm1;
ex k being Nat st
( S₁[k] & ( for n being Nat st S₁[n] holds
k <= n ) ) from NAT_1:sch 5(A1);
then consider k being Nat such that
A2: ( k is_at_least_length_of p & ( for n being Nat st n is_at_least_length_of p holds
k <= n ) ) ;
take k ; :: thesis: ( k is Element of NAT & k is_at_least_length_of p & ( for n being Nat st n is_at_least_length_of p holds
k <= n ) )
thus ( k is Element of NAT & k is_at_least_length_of p & ( for n being Nat st n is_at_least_length_of p holds
k <= n ) ) by A2, ORDINAL1:def 13; :: thesis: verum