let I be set ; :: thesis: for M being non-empty ManySortedSet of I
for X being Element of M holds X = (id M) .. X
let M be non-empty 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;

now :: thesis: for i being object st i in I holds
X . i = ((id M) .. X) . i

let i be object ; :: 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 14;
then g . (X . i) = X . i ;
hence X . i = ((id M) .. X) . i by A2, PRALG_1:def 20; :: thesis: verum

end;

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