let I be set ; :: thesis: for x being ManySortedSet of I holds union {x} = x
let x be ManySortedSet of I; :: thesis: union {x} = x

now :: thesis: for i being object st i in I holds
(union {x}) . i = x . i

let i be object ; :: thesis: ( i in I implies (union {x}) . i = x . i )
assume A1: i in I ; :: thesis: (union {x}) . i = x . i
hence (union {x}) . i = union ({x} . i) by MBOOLEAN:def 2
.= union {(x . i)} by A1, Def1
.= x . i by ZFMISC_1:25 ;
:: thesis: verum

end;

hence union {x} = x ; :: thesis: verum