defpred S₁[ 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 S₁[x,y]

proof

let x be Point of (ZariskiTS B); :: thesis: ex y being Point of (ZariskiTS A) st S₁[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;
S₁[x,y] ;
hence ex y being Point of (ZariskiTS A) st S₁[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 S₁[x,f . x] from FUNCT_2:sch 3(A1);
thus ex b₁ being Function of (ZariskiTS B),(ZariskiTS A) st
for x being Point of (ZariskiTS B) holds b₁ . x = h " x by A2; :: thesis: verum