let x be set ; :: thesis: for f being Function st x in Union (disjoin f) holds
ex y, z being set st x = [y,z]
let f be Function; :: thesis: ( x in Union (disjoin f) implies ex y, z being set st x = [y,z] )
assume x in Union (disjoin f) ; :: thesis: ex y, z being set st x = [y,z]
then consider X being set such that
A1: ( x in X & X in rng (disjoin f) ) by TARSKI:def 4;
consider y being set such that
A2: ( y in dom (disjoin f) & X = (disjoin f) . y ) by A1, FUNCT_1:def 5;
y in dom f by A2, Def3;
then X = [:(f . y),{y}:] by A2, Def3;
hence ex y, z being set st x = [y,z] by A1, RELAT_1:def 1; :: thesis: verum