let f be Function; ( f is union-distributive implies for x, y being set st x in dom f & y in dom f & x \/ y in dom f holds
f . (x \/ y) = (f . x) \/ (f . y) )
assume A1:
f is union-distributive
; for x, y being set st x in dom f & y in dom f & x \/ y in dom f holds
f . (x \/ y) = (f . x) \/ (f . y)
let x, y be set ; ( x in dom f & y in dom f & x \/ y in dom f implies f . (x \/ y) = (f . x) \/ (f . y) )
set X = {x,y};
assume that
A2:
( x in dom f & y in dom f )
and
A3:
x \/ y in dom f
; f . (x \/ y) = (f . x) \/ (f . y)
A4:
union {x,y} = x \/ y
by ZFMISC_1:75;
{x,y} c= dom f
by A2, ZFMISC_1:32;
hence f . (x \/ y) =
union (f .: {x,y})
by A1, A3, A4
.=
union {(f . x),(f . y)}
by A2, FUNCT_1:60
.=
(f . x) \/ (f . y)
by ZFMISC_1:75
;
verum