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 )

then f in { ({i} --> x) where x is Element of X : verum } ;

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

( 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
ex x being Element of X st f = {i} --> x
; :: thesis: 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;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

then f in { ({i} --> x) where x is Element of X : verum } ;

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