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 } )

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

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

then ex x being Element of X st z = {i} --> x ;

hence z in product ({i} --> X) by Th13; :: thesis: verum

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

assume
z in { ({i} --> x) where x is Element of X : verum }
; :: thesis: 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;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

then ex x being Element of X st z = {i} --> x ;

hence z in product ({i} --> X) by Th13; :: thesis: verum