let I be set ; :: thesis: for M being V8() ManySortedSet of I
for X being Element of M holds X = (id M) .. X
let M be V8() ManySortedSet of I; :: thesis: for X being Element of M holds X = (id M) .. X
let X be Element of M; :: thesis: X = (id M) .. X
set F = id M;
A1: dom (id M) = I by PARTFUN1:def 4;

now

let i be set ; :: thesis: ( i in I implies X . i = ((id M) .. X) . i )
reconsider g = (id M) . i as Function ;
assume A2: i in I ; :: thesis: X . i = ((id M) .. X) . i
then ( X . i is Element of M . i & (id M) . i = id (M . i) ) by MSUALG_3:def 1, PBOOLE:def 17;
then g . (X . i) = X . i by A2, FUNCT_1:35;
hence X . i = ((id M) .. X) . i by A1, A2, PRALG_1:def 17; :: thesis: verum

end;

hence X = (id M) .. X by PBOOLE:3; :: thesis: verum