let F, f be Function; :: thesis: for i, xi being set st xi in F . i & f in product F holds

f +* (i,xi) in product F

let i, xi be set ; :: thesis: ( xi in F . i & f in product F implies f +* (i,xi) in product F )

assume A1: xi in F . i ; :: thesis: ( not f in product F or f +* (i,xi) in product F )

assume A2: f in product F ; :: thesis: f +* (i,xi) in product F

A3: for x being object st x in dom F holds

(f +* (i,xi)) . x in F . x

then dom (f +* (i,xi)) = dom F by FUNCT_7:30;

hence f +* (i,xi) in product F by A3, CARD_3:9; :: thesis: verum

f +* (i,xi) in product F

let i, xi be set ; :: thesis: ( xi in F . i & f in product F implies f +* (i,xi) in product F )

assume A1: xi in F . i ; :: thesis: ( not f in product F or f +* (i,xi) in product F )

assume A2: f in product F ; :: thesis: f +* (i,xi) in product F

A3: for x being object st x in dom F holds

(f +* (i,xi)) . x in F . x

proof

dom f = dom F
by A2, CARD_3:9;
let x be object ; :: thesis: ( x in dom F implies (f +* (i,xi)) . x in F . x )

assume A4: x in dom F ; :: thesis: (f +* (i,xi)) . x in F . x

end;assume A4: x in dom F ; :: thesis: (f +* (i,xi)) . x in F . x

then dom (f +* (i,xi)) = dom F by FUNCT_7:30;

hence f +* (i,xi) in product F by A3, CARD_3:9; :: thesis: verum