let I be set ; :: thesis: for M being V8() ManySortedSet of
for X being Element of M holds X = (id M) .. X
let M be V8() ManySortedSet of ; :: 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 )
assume A2: i in I ; :: thesis: X . i = ((id M) .. X) . i
then A3: M . i <> {} ;
A4: X . i is Element of M . i by A2, PBOOLE:def 17;
reconsider g = (id M) . i as Function ;
(id M) . i = id (M . i) by A2, MSUALG_3:def 1;
then g . (X . i) = X . i by A3, A4, 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