let n be Nat; :: thesis:
let X be non empty set ; :: thesis:
let S be non empty Subset-Family of X; :: thesis:
let x be Subset of (Funcs ((Seg n),X)); :: thesis:
let s be Tuple of n,S; :: thesis:
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 = 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:

hereby :: thesis:

assume A2: u in x ; :: thesis:
then A3: u in Funcs ((Seg n),X) ;
reconsider u1 = u as Function by A2;

now :: thesis:

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:

hereby :: thesis:

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

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:

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:

now :: thesis:

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

proof

let t be object ; :: according to TARSKI:def 3 :: thesis:
assume t in rng g ; :: thesis:
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:

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:
assume i in Seg n ; :: thesis:
then i in dom s by FINSEQ_2:124;
hence g . i in s . i by A7; :: thesis:

end;

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

end;

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

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: