let i, I, X be set ; :: thesis: for M being ManySortedSet of st i in I holds
dom (M +* (i .--> X)) = I
let M be ManySortedSet of ; :: 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 4
.= I \/ {i} by FUNCOP_1:19
.= I by A1, ZFMISC_1:46 ; :: thesis: verum