let F, f be Function; 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 ; ( xi in F . i & f in product F implies f +* (i,xi) in product F )
assume A1:
xi in F . i
; ( not f in product F or f +* (i,xi) in product F )
assume A2:
f in product F
; f +* (i,xi) in product F
A3:
for x being object st x in dom F holds
(f +* (i,xi)) . x in F . x
dom f = dom F
by A2, CARD_3:9;
then
dom (f +* (i,xi)) = dom F
by FUNCT_7:30;
hence
f +* (i,xi) in product F
by A3, CARD_3:9; verum