let x, y be set ; :: thesis: for f being Function st x in dom f & y in f . x holds
x .--> y in sproduct f
let f be Function; :: thesis: ( x in dom f & y in f . x implies x .--> y in sproduct f )
assume that
A1: x in dom f and
A2: y in f . x ; :: thesis: x .--> y in sproduct f
A3: dom (x .--> y) = {x} by FUNCOP_1:13;
then A4: dom (x .--> y) c= dom f by A1, ZFMISC_1:31;

now

let z be set ; :: thesis: ( z in dom (x .--> y) implies (x .--> y) . z in f . z )
assume z in dom (x .--> y) ; :: thesis: (x .--> y) . z in f . z
then z = x by A3, TARSKI:def 1;
hence (x .--> y) . z in f . z by A2, FUNCOP_1:72; :: thesis: verum

end;

hence x .--> y in sproduct f by A4, Def9; :: thesis: verum