let F be Function; :: thesis: for x, y, z being set st z in dom (F +* (x .--> y)) & not z in dom F holds
x = z
let x, y, z be set ; :: thesis: ( z in dom (F +* (x .--> y)) & not z in dom F implies x = z )
assume that
A: z in dom (F +* (x .--> y)) and
B: not z in dom F ; :: thesis: x = z
dom (x .--> y) = {x} by FUNCOP_1:19;
then z in (dom F) \/ {x} by A, FUNCT_4:def 1;
then z in {x} by B, XBOOLE_0:def 3;
hence x = z by TARSKI:def 1; :: thesis: verum