set g = Product_dom D;

defpred S_{1}[ Nat] means (Product_dom D) . D is finite ;

D . 0 = (Product_dom D) . 0 by Def10;

then A1: S_{1}[ 0 ]
;

A2: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[n]
from NAT_1:sch 2(A1, A2);

let x be object ; :: according to FINSET_1:def 5 :: thesis: ( not x in NAT or (Product_dom D) . x is finite )

thus ( not x in NAT or (Product_dom D) . x is finite ) by A3; :: thesis: verum

defpred S

D . 0 = (Product_dom D) . 0 by Def10;

then A1: S

A2: for k being Nat st S

S

proof

A3:
for n being Nat holds S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

(Product_dom D) . (k + 1) = [:((Product_dom D) . k),(D . (k + 1)):] by Def10;

hence ( S_{1}[k] implies S_{1}[k + 1] )
; :: thesis: verum

end;(Product_dom D) . (k + 1) = [:((Product_dom D) . k),(D . (k + 1)):] by Def10;

hence ( S

let x be object ; :: according to FINSET_1:def 5 :: thesis: ( not x in NAT or (Product_dom D) . x is finite )

thus ( not x in NAT or (Product_dom D) . x is finite ) by A3; :: thesis: verum