let Y, X be set ; :: thesis: Union (disjoin (Y --> X)) = [:X,Y:]
set f = Y --> X;
A1: ( dom (Y --> X) = Y & ( for x being set st x in Y holds
(Y --> X) . x = X ) ) by FUNCOP_1:13, FUNCOP_1:19;
thus Union (disjoin (Y --> X)) c= [:X,Y:] :: according to XBOOLE_0:def 10 :: thesis: [:X,Y:] c= Union (disjoin (Y --> X))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Union (disjoin (Y --> X)) or x in [:X,Y:] )
assume x in Union (disjoin (Y --> X)) ; :: thesis: x in [:X,Y:]
then consider Z being set such that
A2: ( x in Z & Z in rng (disjoin (Y --> X)) ) by TARSKI:def 4;
consider y being set such that
A3: ( y in dom (disjoin (Y --> X)) & Z = (disjoin (Y --> X)) . y ) by A2, FUNCT_1:def 5;
y in Y by A1, A3, Def3;
then ( Z = [:((Y --> X) . y),{y}:] & (Y --> X) . y = X & X = X & {y} c= Y ) by A1, A3, Def3, ZFMISC_1:37;
then Z c= [:X,Y:] by ZFMISC_1:118;
hence x in [:X,Y:] by A2; :: thesis: verum

end;

let x1, x2 be set ; :: according to RELAT_1:def 3 :: thesis: ( not [x1,x2] in [:X,Y:] or [x1,x2] in Union (disjoin (Y --> X)) )
assume [x1,x2] in [:X,Y:] ; :: thesis: [x1,x2] in Union (disjoin (Y --> X))
then A4: ( x1 in X & x2 in Y ) by ZFMISC_1:106;
then ( (Y --> X) . x2 = X & (disjoin (Y --> X)) . x2 = [:((Y --> X) . x2),{x2}:] & x2 in dom (disjoin (Y --> X)) & x2 in {x2} ) by A1, Def3, TARSKI:def 1;
then ( [x1,x2] in [:((Y --> X) . x2),{x2}:] & [:((Y --> X) . x2),{x2}:] in rng (disjoin (Y --> X)) ) by A4, FUNCT_1:def 5, ZFMISC_1:106;
hence [x1,x2] in Union (disjoin (Y --> X)) by TARSKI:def 4; :: thesis: verum