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

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