defpred S1[ Point of (ZariskiTS B), object ] means $2 = h " $1;
A1: for x being Point of (ZariskiTS B) ex y being Point of (ZariskiTS A) st S1[x,y]
proof
let x be Point of (ZariskiTS B); :: thesis: ex y being Point of (ZariskiTS A) st S1[x,y]
x is prime Ideal of B by Lm44;
then h " x is prime Ideal of A by A0, Th51;
then h " x in Spectrum A ;
then reconsider y = h " x as Point of (ZariskiTS A) by Def7;
S1[x,y] ;
hence ex y being Point of (ZariskiTS A) st S1[x,y] ; :: thesis: verum
end;
consider f being Function of (ZariskiTS B),(ZariskiTS A) such that
A2: for x being Point of (ZariskiTS B) holds S1[x,f . x] from FUNCT_2:sch 3(A1);
 thus ex b1 being Function of (ZariskiTS B),(ZariskiTS A) st
for x being Point of (ZariskiTS B) holds b1 . x = h " x by A2; :: thesis: verum