let X be non empty set ; :: thesis: for i, f being object holds
( f in product ({i} --> X) iff ex x being Element of X st f = {i} --> x )
let i, f be object ; :: thesis: ( f in product ({i} --> X) iff ex x being Element of X st f = {i} --> x )

hereby :: thesis: ( ex x being Element of X st f = {i} --> x implies f in product ({i} --> X) )

assume f in product ({i} --> X) ; :: thesis: ex x being Element of X st f = {i} --> x
then f in { ({i} --> x) where x is Element of X : verum } by Th15;
hence ex x being Element of X st f = {i} --> x ; :: thesis: verum

end;

assume ex x being Element of X st f = {i} --> x ; :: thesis: f in product ({i} --> X)
then f in { ({i} --> x) where x is Element of X : verum } ;
hence f in product ({i} --> X) by Th15; :: thesis: verum