defpred S₁[ Nat] means OuterVx ((((repeat f) . $1) . g),n) = {} ;
A2: ex k being Nat st S₁[k] by A1;
ex k being Nat st
( S₁[k] & ( for n being Nat st S₁[n] holds
k <= n ) ) from NAT_1:sch 5(A2);
then consider k being Nat such that
A3: ( S₁[k] & ( for n being Nat st S₁[n] holds
k <= n ) ) ;
k in NAT by ORDINAL1:def 12;
hence ex b₁ being Element of NAT st
( OuterVx ((((repeat f) . b₁) . g),n) = {} & ( for k being Nat st OuterVx ((((repeat f) . k) . g),n) = {} holds
b₁ <= k ) ) by A3; :: thesis: verum