let I be set ; :: thesis: for f being Function
for M being ManySortedSet of I holds (f +* M) | I = M
let f be Function; :: thesis: for M being ManySortedSet of I holds (f +* M) | I = M
let M be ManySortedSet of I; :: thesis: (f +* M) | I = M
A1: dom (f | I) c= I by RELAT_1:87;
A2: dom M = I by PARTFUN1:def 4;
thus (f +* M) | I = (f | I) +* (M | I) by FUNCT_4:75
.= (f | I) +* M by A2, RELAT_1:98
.= M by A1, A2, FUNCT_4:20 ; :: thesis: verum