let I be set ; for x, y being ManySortedSet of I holds union {{x},{y}} = {x,y}
let x, y be ManySortedSet of I; union {{x},{y}} = {x,y}
now for i being object st i in I holds
(union {{x},{y}}) . i = {x,y} . ilet i be
object ;
( i in I implies (union {{x},{y}}) . i = {x,y} . i )assume A1:
i in I
;
(union {{x},{y}}) . i = {x,y} . ihence (union {{x},{y}}) . i =
union ({{x},{y}} . i)
by MBOOLEAN:def 2
.=
union {({x} . i),({y} . i)}
by A1, Def2
.=
union {{(x . i)},({y} . i)}
by A1, Def1
.=
union {{(x . i)},{(y . i)}}
by A1, Def1
.=
{(x . i),(y . i)}
by ZFMISC_1:26
.=
{x,y} . i
by A1, Def2
;
verum end;
hence
union {{x},{y}} = {x,y}
; verum