theorem :: SRINGS_5:51

for n being 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)) holds
( x is Element of Product (n,S) iff 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 ) ) by Lm1, Lm2;