theorem :: CAYLDICK:5

for z, X being set st z in product <%X%> holds
ex x being set st
( x in X & z = <%x%> )