let x be object ; :: thesis: for f being Function holds
( x in Union (disjoin f) iff ( x `2 in dom f & x `1 in f . (x `2) & x = [(x `1),(x `2)] ) )
let f be Function; :: thesis: ( x in Union (disjoin f) iff ( x `2 in dom f & x `1 in f . (x `2) & x = [(x `1),(x `2)] ) )
thus ( x in Union (disjoin f) implies ( x `2 in dom f & x `1 in f . (x `2) & x = [(x `1),(x `2)] ) ) :: thesis: ( x `2 in dom f & x `1 in f . (x `2) & x = [(x `1),(x `2)] implies x in Union (disjoin f) )

proof

assume x in Union (disjoin f) ; :: thesis: ( x `2 in dom f & x `1 in f . (x `2) & x = [(x `1),(x `2)] )
then consider X being set such that
A1: x in X and
A2: X in rng (disjoin f) by TARSKI:def 4;
consider y being object such that
A3: y in dom (disjoin f) and
A4: X = (disjoin f) . y by A2, FUNCT_1:def 3;
A5: y in dom f by A3, Def3;
then A6: X = [:(f . y),{y}:] by A4, Def3;
then A7: x `1 in f . y by A1, MCART_1:10;
x `2 in {y} by A1, A6, MCART_1:10;
hence ( x `2 in dom f & x `1 in f . (x `2) & x = [(x `1),(x `2)] ) by A1, A5, A6, A7, MCART_1:21, TARSKI:def 1; :: thesis: verum

end;

assume that
A8: x `2 in dom f and
A9: x `1 in f . (x `2) and
A10: x = [(x `1),(x `2)] ; :: thesis: x in Union (disjoin f)
A11: (disjoin f) . (x `2) = [:(f . (x `2)),{(x `2)}:] by A8, Def3;
A12: dom f = dom (disjoin f) by Def3;
x `2 in {(x `2)} by TARSKI:def 1;
then A13: x in [:(f . (x `2)),{(x `2)}:] by A9, A10, ZFMISC_1:87;
[:(f . (x `2)),{(x `2)}:] in rng (disjoin f) by A8, A11, A12, FUNCT_1:def 3;
hence x in Union (disjoin f) by A13, TARSKI:def 4; :: thesis: verum