let x, X be set ; :: thesis: disjoin (x .--> X) = x .--> [:X,{x}:]
A1: ( dom (disjoin ({x} --> X)) = dom ({x} --> X) & dom ({x} --> X) = {x} & dom ({x} --> [:X,{x}:]) = {x} ) by Def3, FUNCOP_1:19;

now

let y be set ; :: thesis: ( y in {x} implies (disjoin ({x} --> X)) . y = ({x} --> [:X,{x}:]) . y )
assume y in {x} ; :: thesis: (disjoin ({x} --> X)) . y = ({x} --> [:X,{x}:]) . y
then ( (disjoin ({x} --> X)) . y = [:(({x} --> X) . y),{y}:] & ({x} --> X) . y = X & ({x} --> [:X,{x}:]) . y = [:X,{x}:] & y = x & X = X ) by A1, Def3, FUNCOP_1:13, TARSKI:def 1;
hence (disjoin ({x} --> X)) . y = ({x} --> [:X,{x}:]) . y ; :: thesis: verum

end;

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