is mentioned by

Thm* s:(A+B) List, x:A. (x mapoutl(s)) (y:A+B. (y s) & isl(y) & x = outl(y))

[member_mapoutl]

In prior sections: mb basic mb list 1 mb list 2

Try larger context: Graphs