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 2;

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 2;

now :: thesis: for i being object st i in I holds

X . i = ((id M) .. X) . i

hence
X = (id M) .. X
; :: thesis: verumX . 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 A1, A2, PRALG_1:def 17; :: thesis: verum

end;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 A1, A2, PRALG_1:def 17; :: thesis: verum