let f be non-empty Function; :: thesis: for X being set
for i, x being object
for g being Function st i in dom f & x in X & g in product f holds
g +* (i,x) in product (f +* (i,X))
let X be set ; :: thesis: for i, x being object
for g being Function st i in dom f & x in X & g in product f holds
g +* (i,x) in product (f +* (i,X))
let i, x be object ; :: thesis: for g being Function st i in dom f & x in X & g in product f holds
g +* (i,x) in product (f +* (i,X))
let g be Function; :: thesis: ( i in dom f & x in X & g in product f implies g +* (i,x) in product (f +* (i,X)) )
assume A1: ( i in dom f & x in X & g in product f ) ; :: thesis: g +* (i,x) in product (f +* (i,X))
A2: dom (g +* (i,x)) = dom g by FUNCT_7:30
.= dom f by A1, CARD_3:9
.= dom (f +* (i,X)) by FUNCT_7:30 ;
for y being object st y in dom (f +* (i,X)) holds
(g +* (i,x)) . y in (f +* (i,X)) . y

proof

let y be object ; :: thesis: ( y in dom (f +* (i,X)) implies (g +* (i,x)) . y in (f +* (i,X)) . y )
assume A3: y in dom (f +* (i,X)) ; :: thesis: (g +* (i,x)) . y in (f +* (i,X)) . y
then A4: y in dom f by FUNCT_7:30;

per cases ( i = y or i <> y ) ;

suppose A5: i = y ; :: thesis: (g +* (i,x)) . y in (f +* (i,X)) . y

y in dom f by A3, FUNCT_7:30;
then y in dom g by A1, CARD_3:9;
then (g +* (i,x)) . y = x by A5, FUNCT_7:31;
hence (g +* (i,x)) . y in (f +* (i,X)) . y by A1, A5, FUNCT_7:31; :: thesis: verum

end;

suppose i <> y ; :: thesis: (g +* (i,x)) . y in (f +* (i,X)) . y

then ( (g +* (i,x)) . y = g . y & (f +* (i,X)) . y = f . y ) by FUNCT_7:32;
hence (g +* (i,x)) . y in (f +* (i,X)) . y by A4, A1, CARD_3:9; :: thesis: verum

end;

end;

end;

hence g +* (i,x) in product (f +* (i,X)) by A2, CARD_3:9; :: thesis: verum