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 i' be set ; :: thesis: ( i' in dom G implies G . i' is finite )
assume i' in dom G ; :: thesis: G . i' is finite
then reconsider i = i' as Element of Seg d by FUNCT_2:def 1;
G . i is finite ;
hence G . i' is finite ; :: thesis: verum

end;

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