let x, y be object ; :: 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) c= dom f by A1, ZFMISC_1:31;

now :: thesis: for z being object st z in dom (x .--> y) holds
(x .--> y) . z in f . z

let z be object ; :: 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 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 A3, Def9; :: thesis: verum