let I be set ; :: thesis: for A being ManySortedSet of holds (id (Union A)) -MSF I,A = id A
let A be ManySortedSet of ; :: thesis: (id (Union A)) -MSF I,A = id A
set f = id (Union A);
set F = (id (Union A)) -MSF I,A;

now

let i be set ; :: thesis: ( i in I implies ((id (Union A)) -MSF I,A) . i = (id A) . i )
assume A1: i in I ; :: thesis: ((id (Union A)) -MSF I,A) . i = (id A) . i
then i in dom A by PARTFUN1:def 4;
then ( A . i in rng A & Union A = union (rng A) ) by CARD_3:def 4, FUNCT_1:def 5;
then ( A . i c= Union A & ((id (Union A)) -MSF I,A) . i = (id (Union A)) | (A . i) & (id A) . i = id (A . i) ) by A1, Def1, MSUALG_3:def 1, ZFMISC_1:92;
hence ((id (Union A)) -MSF I,A) . i = (id A) . i by FUNCT_3:1; :: thesis: verum

end;

hence (id (Union A)) -MSF I,A = id A by PBOOLE:3; :: thesis: verum