let f be Function; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: 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 ;
:: thesis: verum