let f, g be Function of (ZariskiTS B),(ZariskiTS A); :: thesis: ( ( for x being Point of (ZariskiTS B) holds f . x = h " x ) & ( for x being Point of (ZariskiTS B) holds g . x = h " x ) implies f = g )
assume that
A3: for x being Point of (ZariskiTS B) holds f . x = h " x and
A4: for x being Point of (ZariskiTS B) holds g . x = h " x ; :: thesis: f = g
now :: thesis: for x being Point of (ZariskiTS B) holds f . x = g . x
let x be Point of (ZariskiTS B); :: thesis: f . x = g . x
f . x = h " x by A3;
hence f . x = g . x by A4; :: thesis: verum
end;
hence f = g ; :: thesis: verum