set e = the Element of US2;
set f = US1 --> the Element of US2;
for V being Element of the entourages of US2 ex U being Element of the entourages of US1 st
for x, y being object st [x,y] in U holds
[((US1 --> the Element of US2) . x),((US1 --> the Element of US2) . y)] in V
proof
let V be
Element of the
entourages of
US2;
ex U being Element of the entourages of US1 st
for x, y being object st [x,y] in U holds
[((US1 --> the Element of US2) . x),((US1 --> the Element of US2) . y)] in V
per cases
( [ the Element of US2, the Element of US2] in V or not [ the Element of US2, the Element of US2] in V )
;
suppose A1:
[ the Element of US2, the Element of US2] in V
;
ex U being Element of the entourages of US1 st
for x, y being object st [x,y] in U holds
[((US1 --> the Element of US2) . x),((US1 --> the Element of US2) . y)] in Vset U = the
Element of the
entourages of
US1;
take
the
Element of the
entourages of
US1
;
for x, y being object st [x,y] in the Element of the entourages of US1 holds
[((US1 --> the Element of US2) . x),((US1 --> the Element of US2) . y)] in Vthus
for
x,
y being
object st
[x,y] in the
Element of the
entourages of
US1 holds
[((US1 --> the Element of US2) . x),((US1 --> the Element of US2) . y)] in V
verumproof
let x,
y be
object ;
( [x,y] in the Element of the entourages of US1 implies [((US1 --> the Element of US2) . x),((US1 --> the Element of US2) . y)] in V )
assume A2:
[x,y] in the
Element of the
entourages of
US1
;
[((US1 --> the Element of US2) . x),((US1 --> the Element of US2) . y)] in V
consider a,
b being
object such that A3:
a in the
carrier of
US1
and A4:
b in the
carrier of
US1
and A5:
[x,y] = [a,b]
by A2, ZFMISC_1:def 2;
A6:
(
x = a &
y = b )
by A5, XTUPLE_0:1;
(US1 --> the Element of US2) . b = the
Element of
US2
by A4, FUNCOP_1:7;
hence
[((US1 --> the Element of US2) . x),((US1 --> the Element of US2) . y)] in V
by A1, A6, A3, FUNCOP_1:7;
verum
end; end; end;
end;
then
US1 --> the Element of US2 is uniformly_continuous
;
hence
ex b1 being Function of US1,US2 st b1 is uniformly_continuous
; verum