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; :: thesis: 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 ; :: thesis: 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
set U = the Element of the entourages of US1;
take the Element of the entourages of US1 ; :: thesis: 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
thus 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 :: thesis: verum
proof
let x, y be object ; :: thesis: ( [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 ; :: thesis: [((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; :: thesis: verum
end;
end;
suppose A8: not [ the Element of US2, the Element of US2] in V ; :: thesis: 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
US2 is axiom_U1 ;
then A9: id the carrier of US2 c= V ;
[ the Element of US2, the Element of US2] in id the carrier of US2 by RELAT_1:def 10;
hence 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 by A8, A9; :: thesis: verum
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 ; :: thesis: verum