let x be set ; :: thesis: for f being Function st x in dom <:f:> holds
<:f:> . x is Function
let f be Function; :: thesis: ( x in dom <:f:> implies <:f:> . x is Function )
A1: rng <:f:> c= product (rngs f) by Th49;
assume x in dom <:f:> ; :: thesis: <:f:> . x is Function
then <:f:> . x in rng <:f:> by FUNCT_1:def 5;
then ex g being Function st
( <:f:> . x = g & dom g = dom (rngs f) & ( for x being set st x in dom (rngs f) holds
g . x in (rngs f) . x ) ) by A1, CARD_3:def 5;
hence <:f:> . x is Function ; :: thesis: verum