let x be object ; :: thesis: for f being Function st x in Union (disjoin f) holds
ex y, z being object st x = [y,z]
let f be Function; :: thesis: ( x in Union (disjoin f) implies ex y, z being object st x = [y,z] )
assume x in Union (disjoin f) ; :: thesis: ex y, z being object st x = [y,z]
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;
y in dom f by A3, Def3;
then X = [:(f . y),{y}:] by A4, Def3;
hence ex y, z being object st x = [y,z] by A1, RELAT_1:def 1; :: thesis: verum