let X be non empty set ; :: thesis: for i being object holds product ({i} --> X) = { ({i} --> x) where x is Element of X : verum }
let i be object ; :: thesis: product ({i} --> X) = { ({i} --> x) where x is Element of X : verum }
set S = { ({i} --> x) where x is Element of X : verum } ;
for z being object holds
( z in product ({i} --> X) iff z in { ({i} --> x) where x is Element of X : verum } )

proof

let z be object ; :: thesis: ( z in product ({i} --> X) iff z in { ({i} --> x) where x is Element of X : verum } )

hereby :: thesis: ( z in { ({i} --> x) where x is Element of X : verum } implies z in product ({i} --> X) )

assume z in product ({i} --> X) ; :: thesis: z in { ({i} --> x) where x is Element of X : verum }
then consider f being Function such that
A1: ( z = f & dom f = dom ({i} --> X) ) and
A2: for y being object st y in dom ({i} --> X) holds
f . y in ({i} --> X) . y by CARD_3:def 5;
A3: dom f = {i} by A1;
for y being object st y in dom f holds
f . y = f . i by A1, TARSKI:def 1;
then A4: f = {i} --> (f . i) by A3, FUNCOP_1:11;
i in dom ({i} --> X) by TARSKI:def 1;
then f . i in ({i} --> X) . i by A2;
then f . i in (i .--> X) . i by FUNCOP_1:def 9;
then f . i in X by FUNCOP_1:72;
hence z in { ({i} --> x) where x is Element of X : verum } by A1, A4; :: thesis: verum

end;

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

end;

hence product ({i} --> X) = { ({i} --> x) where x is Element of X : verum } by TARSKI:2; :: thesis: verum