let n be Nat; for S being non empty Subset-Family of REAL
for x being Subset of (REAL n) holds
( x is Element of Product (n,S) iff ex s being Tuple of n,S st
for t being Element of REAL n holds
( ( for i being Nat st i in Seg n holds
t . i in s . i ) iff t in x ) )
let S be non empty Subset-Family of REAL; for x being Subset of (REAL n) holds
( x is Element of Product (n,S) iff ex s being Tuple of n,S st
for t being Element of REAL n holds
( ( for i being Nat st i in Seg n holds
t . i in s . i ) iff t in x ) )
let x be Subset of (REAL n); ( x is Element of Product (n,S) iff ex s being Tuple of n,S st
for t being Element of REAL n holds
( ( for i being Nat st i in Seg n holds
t . i in s . i ) iff t in x ) )
A1:
x is Subset of (Funcs ((Seg n),REAL))
by FINSEQ_2:93;
thus
( x is Element of Product (n,S) implies ex s being Tuple of n,S st
for t being Element of REAL n holds
( ( for i being Nat st i in Seg n holds
t . i in s . i ) iff t in x ) )
( ex s being Tuple of n,S st
for t being Element of REAL n holds
( ( for i being Nat st i in Seg n holds
t . i in s . i ) iff t in x ) implies x is Element of Product (n,S) )
thus
( ex s being Tuple of n,S st
for t being Element of REAL n holds
( ( for i being Nat st i in Seg n holds
t . i in s . i ) iff t in x ) implies x is Element of Product (n,S) )
verum