diff --git a/theories/classical_sets.v b/theories/classical_sets.v
index df3290262..1eb1cf29f 100644
--- a/theories/classical_sets.v
+++ b/theories/classical_sets.v
@@ -208,10 +208,18 @@ Arguments mkset _ _ _ /.
 
 Notation "[ 'set' x : T | P ]" := (mkset (fun x : T => P)) : classical_set_scope.
 Notation "[ 'set' x | P ]" := [set x : _ | P] : classical_set_scope.
+
+Definition image {T rT} (A : set T) (f : T -> rT) :=
+  [set y | exists2 x, A x & f x = y].
+Arguments image _ _ _ _ _ /.
 Notation "[ 'set' E | x 'in' A ]" :=
-  [set y | exists2 x, A x & E = y] : classical_set_scope.
+  (image A (fun x => E)) : classical_set_scope.
+
+Definition image2 {TA TB rT} (A : set TA) (B : set TB) (f : TA -> TB -> rT) :=
+  [set z | exists2 x, A x & exists2 y, B y & f x y = z].
+Arguments image2 _ _ _ _ _ _ _ /.
 Notation "[ 'set' E | x 'in' A & y 'in' B ]" :=
-  [set z | exists2 x, A x & exists2 y, B y & E = z] : classical_set_scope.
+  (image2 A B (fun x y => E)) : classical_set_scope.
 
 Section basic_definitions.
 Context {T rT : Type}.
@@ -280,7 +288,7 @@ Notation "A `<` B" := (proper A B) : classical_set_scope.
 
 Notation "A `<=>` B" := ((A `<=` B) /\ (B `<=` A)) : classical_set_scope.
 Notation "f @^-1` A" := (preimage f A) : classical_set_scope.
-Notation "f @` A" := [set f x | x in A] (only parsing) : classical_set_scope.
+Notation "f @` A" := (image A f) (only parsing) : classical_set_scope.
 Notation "A !=set0" := (nonempty A) : classical_set_scope.
 
 Lemma eq_set T (P Q : T -> Prop) : (forall x : T, P x = Q x) ->
diff --git a/theories/normedtype.v b/theories/normedtype.v
index 4478bfc06..d8831cdea 100644
--- a/theories/normedtype.v
+++ b/theories/normedtype.v
@@ -3544,7 +3544,7 @@ move=> C D FC f_D; have {}f_D :
     move=> g Pg; apply: sED => i j; rewrite ord1 row_simpl'.
     by have /getPex [_ /(_ _ (Pg j))] := exPj j.
   split; last by move=> j; have /getPex [[]] := exPj j.
-  exists [set [set g | forall j, get (Pj j) (g j)] | k in 'I_n.+1];
+  exists [set [set g | forall j, get (Pj j) (g j)] | k in [set x | 'I_n.+1 x]];
     last first.
     rewrite predeqE => g; split; first by move=> [_ [_ _ <-]].
     move=> Pg; exists [set g | forall j, get (Pj j) (g j)] => //.