let d be non zero Nat; :: thesis: for x being Element of REAL d
for G being Grating of d holds
( x in product G iff for i being Element of Seg d holds x . i in G . i )
let x be Element of REAL d; :: thesis: for G being Grating of d holds
( x in product G iff for i being Element of Seg d holds x . i in G . i )
let G be Grating of d; :: thesis: ( x in product G iff for i being Element of Seg d holds x . i in G . i )
x is Function of (Seg d),REAL by Def3;
then A1: dom x = Seg d by FUNCT_2:def 1;
A2: dom G = Seg d by FUNCT_2:def 1;
hence ( x in product G implies for i being Element of Seg d holds x . i in G . i ) by CARD_3:9; :: thesis: ( ( for i being Element of Seg d holds x . i in G . i ) implies x in product G )
assume for i being Element of Seg d holds x . i in G . i ; :: thesis: x in product G
then for i being object st i in Seg d holds
x . i in G . i ;
hence x in product G by A1, A2, CARD_3:9; :: thesis: verum