∀ f x y, x = y ⇒ (f x) = (f y)

Theorem eq_f : forall A, forall B, forall (f:(A -> B)), forall (x:A), forall (y:A), (eq (A) x y) -> eq (B) (f x) (f y).

theorem eq_f : \forall A. \forall B. \forall (f:A -> B). \forall (x:A). \forall (y:A). ((eq) (A) x y) -> (eq) (B) (f x) (f y).

theorem eq_f : forall (A : Type) , forall (B : Type) , forall (f:(A) -> B) , forall (x:A) , forall (y:A) , ((((logic.eq_) (A)) (x)) (y)) -> (((logic.eq_) (B)) ((f) (x))) ((f) (y)).

eq_f [A:TYPE+,B:TYPE+] : LEMMA (FORALL(f:[A -> B]):(FORALL(x:A):(FORALL(y:A):(logic_sttfa.eq[A](x)(y) => logic_sttfa.eq[B](f(x))(f(y))))))

Printing for OpenTheory is not working at the moment.