let S be functional set ; :: thesis: for f being Function
for i being set st f in S & i in dom (product" S) holds
f . i in (product" S) . i
let F be Function; :: thesis: for i being set st F in S & i in dom (product" S) holds
F . i in (product" S) . i
let i be set ; :: thesis: ( F in S & i in dom (product" S) implies F . i in (product" S) . i )
assume A1: F in S ; :: thesis: ( not i in dom (product" S) or F . i in (product" S) . i )
assume i in dom (product" S) ; :: thesis: F . i in (product" S) . i
then (product" S) . i = { (f . i) where f is Element of S : verum } by A1, Th73;
hence F . i in (product" S) . i by A1; :: thesis: verum