let x, y be object ; for I being set holds union (I --> {{x},{y}}) = I --> {x,y}
let I be set ; union (I --> {{x},{y}}) = I --> {x,y}
now for i being object st i in I holds
(union (I --> {{x},{y}})) . i = (I --> {x,y}) . ilet i be
object ;
( i in I implies (union (I --> {{x},{y}})) . i = (I --> {x,y}) . i )assume A1:
i in I
;
(union (I --> {{x},{y}})) . i = (I --> {x,y}) . ihence (union (I --> {{x},{y}})) . i =
union ((I --> {{x},{y}}) . i)
by Def2
.=
union {{x},{y}}
by A1, FUNCOP_1:7
.=
{x,y}
by ZFMISC_1:26
.=
(I --> {x,y}) . i
by A1, FUNCOP_1:7
;
verum end;
hence
union (I --> {{x},{y}}) = I --> {x,y}
; verum