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:58;
A2: dom M = I by PARTFUN1:def 2;
thus (f +* M) | I = (f | I) +* (M | I) by FUNCT_4:71
.= (f | I) +* M by A2, RELAT_1:69
.= M by A1, A2, FUNCT_4:19 ; :: thesis: verum