let S be functional with_common_domain set ; :: thesis: for f being Function
for i being set st f in S & i in dom f holds
f . i in (product" S) . i
let f be Function; :: thesis: for i being set st f in S & i in dom f holds
f . i in (product" S) . i
let i be set ; :: thesis: ( f in S & i in dom f implies f . i in (product" S) . i )
assume that
Z1: f in S and
Z2: i in dom f ; :: thesis: f . i in (product" S) . i
dom f = dom (product" S) by Z1, Th150;
hence f . i in (product" S) . i by Z1, Z2, Th151; :: thesis: verum