let n be Nat; :: thesis: 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; :: thesis: 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); :: thesis: ( 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 ) ) :: thesis: ( 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) )

proof

assume x is Element of Product (n,S) ; :: thesis: 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 )
then consider s being Tuple of n,S such that
A2: for t being Element of Funcs ((Seg n),REAL) holds
( ( for i being Nat st i in Seg n holds
t . i in s . i ) iff t in x ) by Lm1;
take s ; :: thesis: 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 )
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 )

proof

let t be Element of REAL n; :: thesis: ( ( for i being Nat st i in Seg n holds
t . i in s . i ) iff t in x )
t is Element of Funcs ((Seg n),REAL) by FINSEQ_2:93;
hence ( ( for i being Nat st i in Seg n holds
t . i in s . i ) iff t in x ) by A2; :: thesis: verum

end;

hence 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 ) ; :: thesis: verum

end;

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) ) :: thesis: verum

proof

given s being Tuple of n,S such that A3: 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 ) ; :: thesis: x is Element of Product (n,S)
ex s being Tuple of n,S st
for t being Element of Funcs ((Seg n),REAL) holds
( ( for i being Nat st i in Seg n holds
t . i in s . i ) iff t in x )

proof

take s ; :: thesis: for t being Element of Funcs ((Seg n),REAL) holds
( ( for i being Nat st i in Seg n holds
t . i in s . i ) iff t in x )
let t be Element of Funcs ((Seg n),REAL); :: thesis: ( ( for i being Nat st i in Seg n holds
t . i in s . i ) iff t in x )
t is Element of REAL n by FINSEQ_2:93;
hence ( ( for i being Nat st i in Seg n holds
t . i in s . i ) iff t in x ) by A3; :: thesis: verum

end;

hence x is Element of Product (n,S) by A1, Lm2; :: thesis: verum

end;