let n be Nat; :: thesis: for X being non empty set
for S being non empty Subset-Family of X
for x being Subset of (Funcs ((Seg n),X))
for s being Tuple of n,S st ( for t being Element of Funcs ((Seg n),X) holds
( t in x iff for i being Nat st i in Seg n holds
t . i in s . i ) ) holds
x is Element of Product (n,S)
let X be non empty set ; :: thesis: for S being non empty Subset-Family of X
for x being Subset of (Funcs ((Seg n),X))
for s being Tuple of n,S st ( for t being Element of Funcs ((Seg n),X) holds
( t in x iff for i being Nat st i in Seg n holds
t . i in s . i ) ) holds
x is Element of Product (n,S)
let S be non empty Subset-Family of X; :: thesis: for x being Subset of (Funcs ((Seg n),X))
for s being Tuple of n,S st ( for t being Element of Funcs ((Seg n),X) holds
( t in x iff for i being Nat st i in Seg n holds
t . i in s . i ) ) holds
x is Element of Product (n,S)
let x be Subset of (Funcs ((Seg n),X)); :: thesis: for s being Tuple of n,S st ( for t being Element of Funcs ((Seg n),X) holds
( t in x iff for i being Nat st i in Seg n holds
t . i in s . i ) ) holds
x is Element of Product (n,S)
let s be Tuple of n,S; :: thesis: ( ( for t being Element of Funcs ((Seg n),X) holds
( t in x iff for i being Nat st i in Seg n holds
t . i in s . i ) ) implies x is Element of Product (n,S) )
assume A1: for t being Element of Funcs ((Seg n),X) holds
( t in x iff for i being Nat st i in Seg n holds
t . i in s . i ) ; :: thesis: x is Element of Product (n,S)
x = product s

proof

for u being object holds
( u in x iff ex g being Function st
( u = g & dom g = dom s & ( for v being object st v in dom s holds
g . v in s . v ) ) )

proof

let u be object ; :: thesis: ( u in x iff ex g being Function st
( u = g & dom g = dom s & ( for v being object st v in dom s holds
g . v in s . v ) ) )

hereby :: thesis: ( ex g being Function st
( u = g & dom g = dom s & ( for v being object st v in dom s holds
g . v in s . v ) ) implies u in x )

assume A2: u in x ; :: thesis: ex g being Function st
( u = g & dom g = dom s & ( for v being object st v in dom s holds
g . v in s . v ) )
then A3: u in Funcs ((Seg n),X) ;
reconsider u1 = u as Function by A2;

now :: thesis: ( dom u1 = dom s & ( for v being object st v in dom s holds
u1 . v in s . v ) )

u1 in n -tuples_on X by A3, FINSEQ_2:93;
then dom u1 = Seg n by FINSEQ_1:89;
hence dom u1 = dom s by FINSEQ_2:124; :: thesis: for v being object st v in dom s holds
u1 . v in s . v

hereby :: thesis: verum

let v be object ; :: thesis: ( v in dom s implies u1 . v in s . v )
assume v in dom s ; :: thesis: u1 . v in s . v
then v in Seg n by FINSEQ_2:124;
hence u1 . v in s . v by A1, A2; :: thesis: verum

end;

end;

hence ex g being Function st
( u = g & dom g = dom s & ( for v being object st v in dom s holds
g . v in s . v ) ) ; :: thesis: verum

end;

given g being Function such that A5: u = g and
A6: dom g = dom s and
A7: for v being object st v in dom s holds
g . v in s . v ; :: thesis: u in x

now :: thesis: ( dom g = Seg n & rng g c= X )

thus dom g = Seg n by A6, FINSEQ_2:124; :: thesis: rng g c= X
thus rng g c= X :: thesis: verum

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in rng g or t in X )
assume t in rng g ; :: thesis: t in X
then consider a being object such that
A8: a in dom g and
A9: t = g . a by FUNCT_1:def 3;
( g . a in s . a & s . a in rng s & rng s c= S ) by A6, A8, A7, FUNCT_1:3;
then ( g . a in s . a & s . a in S & union S c= union (bool X) ) by ZFMISC_1:77;
hence t in X by A9; :: thesis: verum

end;

end;

then A10: g is Element of Funcs ((Seg n),X) by FUNCT_2:def 2;
for i being Nat st i in Seg n holds
g . i in s . i

proof

let i be Nat; :: thesis: ( i in Seg n implies g . i in s . i )
assume i in Seg n ; :: thesis: g . i in s . i
then i in dom s by FINSEQ_2:124;
hence g . i in s . i by A7; :: thesis: verum

end;

hence u in x by A1, A5, A10; :: thesis: verum

end;

hence x = product s by CARD_3:def 5; :: thesis: verum

end;

then x in { (product f) where f is Tuple of n,S : verum } ;
hence x is Element of Product (n,S) by Th38; :: thesis: verum