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
A1: f in S and
A2: i in dom f ; :: thesis: f . i in (product" S) . i
dom f = dom (product" S) by A1, Th97;
hence f . i in (product" S) . i by A1, A2, Th98; :: thesis: verum