set f = n GeoSeq ;
let y be object ; :: according to RELAT_1:def 19,TARSKI:def 3 :: thesis: ( not y in rng (n GeoSeq) or y in NAT )
assume y in rng (n GeoSeq) ; :: thesis: y in NAT
then consider x being object such that
A1: x in dom (n GeoSeq) and
A2: y = (n GeoSeq) . x by FUNCT_1:def 3;
A3: dom (n GeoSeq) = NAT by SEQ_1:1;
defpred S₁[ Nat] means (n GeoSeq) . n in NAT ;
(n GeoSeq) . 0 = 1 by PREPOWER:3;
then A4: S₁[ 0 ] ;
A5: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A6: S₁[k] ; :: thesis: S₁[k + 1]
(n GeoSeq) . (k + 1) = ((n GeoSeq) . k) * n by PREPOWER:3;
then (n GeoSeq) . (k + 1) is natural by A6;
hence S₁[k + 1] ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A4, A5);
hence y in NAT by A1, A2, A3; :: thesis: verum