let n be Nat; :: thesis: for X being non empty set
for S being non empty Subset-Family of X
for x being Element of Product (n,S) ex s being Tuple of n,S st
for t being Element of Funcs ((Seg n),X) holds
( ( for i being Nat st i in Seg n holds
t . i in s . i ) iff t in x )
let X be non empty set ; :: thesis: for S being non empty Subset-Family of X
for x being Element of Product (n,S) ex s being Tuple of n,S st
for t being Element of Funcs ((Seg n),X) 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 X; :: thesis: for x being Element of Product (n,S) ex s being Tuple of n,S st
for t being Element of Funcs ((Seg n),X) holds
( ( for i being Nat st i in Seg n holds
t . i in s . i ) iff t in x )
let x be Element of Product (n,S); :: thesis: ex s being Tuple of n,S st
for t being Element of Funcs ((Seg n),X) holds
( ( for i being Nat st i in Seg n holds
t . i in s . i ) iff t in x )
consider g being Function such that
A1: x = product g and
A2: g in product ((Seg n) --> S) by Def2;
g in n -tuples_on S by A2, Th8;
then reconsider g = g as Tuple of n,S by FINSEQ_2:131;
take g ; :: thesis: for t being Element of Funcs ((Seg n),X) holds
( ( for i being Nat st i in Seg n holds
t . i in g . i ) iff t in x )
for t being Element of Funcs ((Seg n),X) holds
( ( for i being Nat st i in Seg n holds
t . i in g . i ) iff t in x )
proof
let t be Element of Funcs ((Seg n),X); :: thesis: ( ( for i being Nat st i in Seg n holds
t . i in g . i ) iff t in x )
hereby :: thesis: ( t in x implies for i being Nat st i in Seg n holds
t . i in g . i )
assume A3: for i being Nat st i in Seg n holds
t . i in g . i ; :: thesis: t in x
t in Funcs ((Seg n),X) ;
then t in n -tuples_on X by FINSEQ_2:93;
then dom t = Seg n by FINSEQ_1:89;
then A4: dom t = dom g by FINSEQ_2:124;
for i being object st i in dom g holds
t . i in g . i
proof
let i be object ; :: thesis: ( i in dom g implies t . i in g . i )
assume i in dom g ; :: thesis: t . i in g . i
then i in Seg n by FINSEQ_2:124;
hence t . i in g . i by A3; :: thesis: verum
end;
hence t in x by A1, A4, CARD_3:def 5; :: thesis: verum
end;
assume A5: t in x ; :: thesis: for i being Nat st i in Seg n holds
t . i in g . i
hereby :: thesis: verum
let i be Nat; :: thesis: ( i in Seg n implies t . i in g . i )
assume A6: i in Seg n ; :: thesis: t . i in g . i
consider h being Function such that
A7: t = h and
dom h = dom g and
A8: for u being object st u in dom g holds
h . u in g . u by A5, A1, CARD_3:def 5;
i in dom g by A6, FINSEQ_2:124;
hence t . i in g . i by A8, A7; :: thesis: verum
end;
end;
hence for t being Element of Funcs ((Seg n),X) holds
( ( for i being Nat st i in Seg n holds
t . i in g . i ) iff t in x ) ; :: thesis: verum