let n be Nat; 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 ; 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; 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)); 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; ( ( 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 )
; x is Element of Product (n,S)
x = product s
then
x in { (product f) where f is Tuple of n,S : verum }
;
hence
x is Element of Product (n,S)
by Th38; verum