let i be object ; :: thesis: for I being set
for X being object
for M being ManySortedSet of I st i in I holds
dom (M +* (i .--> X)) = I
let I be set ; :: thesis: for X being object
for M being ManySortedSet of I st i in I holds
dom (M +* (i .--> X)) = I
let X be object ; :: thesis: for M being ManySortedSet of I st i in I holds
dom (M +* (i .--> X)) = I
let M be ManySortedSet of I; :: thesis: ( i in I implies dom (M +* (i .--> X)) = I )
assume A1: i in I ; :: thesis: dom (M +* (i .--> X)) = I
thus dom (M +* (i .--> X)) = (dom M) \/ (dom (i .--> X)) by FUNCT_4:def 1
.= I \/ (dom (i .--> X)) by PARTFUN1:def 2
.= I \/ {i}
.= I by A1, ZFMISC_1:40 ; :: thesis: verum