set f = i GeoSeq ;
let y be object ; :: according to RELAT_1:def 19,TARSKI:def 3 :: thesis: ( not y in rng (i GeoSeq) or y in INT )
assume y in rng (i GeoSeq) ; :: thesis: y in INT
then consider x being object such that
A1: x in dom (i GeoSeq) and
A2: y = (i GeoSeq) . x by FUNCT_1:def 3;
A3: dom (i GeoSeq) = NAT by SEQ_1:1;
defpred S₁[ Nat] means (i GeoSeq) . i in INT ;
(i GeoSeq) . 0 = 1 by PREPOWER:3;
then A4: S₁[ 0 ] by INT_1:def 1;
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]
(i GeoSeq) . (k + 1) = ((i GeoSeq) . k) * i by PREPOWER:3;
then (i GeoSeq) . (k + 1) is integer 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 INT by A1, A2, A3; :: thesis: verum