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
.= 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 ;
then y in dom g by ;
then (g +* (i,x)) . y = x by ;
hence (g +* (i,x)) . y in (f +* (i,X)) . y by ; :: 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 ; :: thesis: verum
end;
end;
end;
hence g +* (i,x) in product (f +* (i,X)) by ; :: thesis: verum