set g = Product_dom D;
defpred S₁[ Nat] means (Product_dom D) . D is finite ;
D . 0 = (Product_dom D) . 0 by Def10;
then A1: S₁[ 0 ] ;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
(Product_dom D) . (k + 1) = [:((Product_dom D) . k),(D . (k + 1)):] by Def10;
hence ( S₁[k] implies S₁[k + 1] ) ; :: thesis: verum

end;

A3: for n being Nat holds S₁[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