c:Collection(T), f:(T
T'), x:T'.
x 
< f(y) | y c > 
(
y:T. y c & x = f(y)) c > (y) == x:T. x c & y = f(x) T'
is mentioned by
|
Thm* c:Collection(T), f:(TT'), x:T'.
x < f(y) | y c > (y:T. y c & x = f(y)) | [member_col_map] |
Try larger context: GenAutomata