let A, B be non degenerated commutative Ring; :: thesis: for h being Function of A,B st h is RingHomomorphism holds
Spec h is continuous
let h be Function of A,B; :: thesis: ( h is RingHomomorphism implies Spec h is continuous )
assume A1: h is RingHomomorphism ; :: thesis: Spec h is continuous
for P1 being Subset of (ZariskiTS A) st P1 is closed holds
(Spec h) " P1 is closed

proof

let P1 be Subset of (ZariskiTS A); :: thesis: ( P1 is closed implies (Spec h) " P1 is closed )
assume P1 is closed ; :: thesis: (Spec h) " P1 is closed
then consider E being non empty Subset of A such that
A3: P1 = PrimeIdeals (A,E) by Def7;
A4: dom h = the carrier of A by FUNCT_2:def 1;
(Spec h) " P1 = PrimeIdeals (B,(h .: E)) by A3, A1, Th52;
then consider E1 being non empty Subset of B such that
E1 = h .: E and
A5: (Spec h) " P1 = PrimeIdeals (B,E1) by A4;
thus (Spec h) " P1 is closed by A5, Def7; :: thesis: verum

end;

hence Spec h is continuous by PRE_TOPC:def 6; :: thesis: verum