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

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