let x be set ; :: 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 set such that
A3: y in dom (disjoin f) and
A4: X = (disjoin f) . y by A2, FUNCT_1:def 5;
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:23, 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:106;
[:(f . (x `2 )),{(x `2 )}:] in rng (disjoin f) by A8, A11, A12, FUNCT_1:def 5;
hence x in Union (disjoin f) by A13, TARSKI:def 4; :: thesis: verum