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
A1: z in dom (F +* (x .--> y)) and
A2: not z in dom F ; :: thesis: x = z
dom (x .--> y) = {x} ;
then z in (dom F) \/ {x} by A1, FUNCT_4:def 1;
then z in {x} by A2, XBOOLE_0:def 3;
hence x = z by TARSKI:def 1; :: thesis: verum