let x be object ; :: thesis: for X being set holds disjoin (x .--> X) = x .--> [:X,{x}:]
let X be set ; :: thesis: disjoin (x .--> X) = x .--> [:X,{x}:]
A1: dom (disjoin ({x} --> X)) = dom ({x} --> X) by Def3;
A2: dom ({x} --> X) = {x} ;

now :: thesis: for y being object st y in {x} holds
(disjoin ({x} --> X)) . y = ({x} --> [:X,{x}:]) . y

let y be object ; :: thesis: ( y in {x} implies (disjoin ({x} --> X)) . y = ({x} --> [:X,{x}:]) . y )
assume A4: y in {x} ; :: thesis: (disjoin ({x} --> X)) . y = ({x} --> [:X,{x}:]) . y
then A5: (disjoin ({x} --> X)) . y = [:(({x} --> X) . y),{y}:] by A2, Def3;
A6: ({x} --> X) . y = X by A4, FUNCOP_1:7;
({x} --> [:X,{x}:]) . y = [:X,{x}:] by A4, FUNCOP_1:7;
hence (disjoin ({x} --> X)) . y = ({x} --> [:X,{x}:]) . y by A4, A5, A6, TARSKI:def 1; :: thesis: verum

end;

hence disjoin (x .--> X) = x .--> [:X,{x}:] by A1; :: thesis: verum