let I be set ; :: thesis: for A being ManySortedSet of I holds (id (Union A)) -MSF I,A = id A
let A be ManySortedSet of I; :: 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 )
A1: Union A = union (rng A) by CARD_3:def 4;
assume A2: i in I ; :: thesis: ((id (Union A)) -MSF I,A) . i = (id A) . i
then i in dom A by PARTFUN1:def 4;
then A3: A . i in rng A by FUNCT_1:def 5;
( ((id (Union A)) -MSF I,A) . i = (id (Union A)) | (A . i) & (id A) . i = id (A . i) ) by A2, Def1, MSUALG_3:def 1;
hence ((id (Union A)) -MSF I,A) . i = (id A) . i by A3, A1, FUNCT_3:1, ZFMISC_1:92; :: thesis: verum

end;

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