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

let i be set ; :: 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 by PBOOLE:3; :: thesis: verum