let d be non zero Element of NAT ; :: thesis: for G being Grating of d holds product G is finite
let G be Grating of d; :: thesis: product G is finite

now

let i9 be set ; :: thesis: ( i9 in dom G implies G . i9 is finite )
assume i9 in dom G ; :: thesis: G . i9 is finite
then reconsider i = i9 as Element of Seg d by FUNCT_2:def 1;
G . i is finite ;
hence G . i9 is finite ; :: thesis: verum

end;

hence product G is finite by MSSCYC_1:1; :: thesis: verum