defpred S_{1}[ Nat] means OuterVx ((((repeat f) . $1) . g),n) = {} ;

A2: ex k being Nat st S_{1}[k]
by A1;

ex k being Nat st

( S_{1}[k] & ( for n being Nat st S_{1}[n] holds

k <= n ) ) from NAT_1:sch 5(A2);

then consider k being Nat such that

A3: ( S_{1}[k] & ( for n being Nat st S_{1}[n] holds

k <= n ) ) ;

k in NAT by ORDINAL1:def 12;

hence ex b_{1} being Element of NAT st

( OuterVx ((((repeat f) . b_{1}) . g),n) = {} & ( for k being Nat st OuterVx ((((repeat f) . k) . g),n) = {} holds

b_{1} <= k ) )
by A3; :: thesis: verum

A2: ex k being Nat st S

ex k being Nat st

( S

k <= n ) ) from NAT_1:sch 5(A2);

then consider k being Nat such that

A3: ( S

k <= n ) ) ;

k in NAT by ORDINAL1:def 12;

hence ex b

( OuterVx ((((repeat f) . b

b