let x, 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} by FUNCOP_1:19;
A3: dom ({x} --> [:X,{x}:]) = {x} by FUNCOP_1:19;

now

let y be set ; :: 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:13;
({x} --> [:X,{x}:]) . y = [:X,{x}:] by A4, FUNCOP_1:13;
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, A2, A3, FUNCT_1:9; :: thesis: verum