let T be non empty normal TopSpace; for A, B being closed Subset of T st A <> {} & A misses B holds
for G being Rain of A,B ex F being Function of DOM,(bool the carrier of T) st
for x being Real st x in DOM holds
( ( x in halfline 0 implies F . x = {} ) & ( x in right_open_halfline 1 implies F . x = the carrier of T ) & ( x in DYADIC implies for n being Nat st x in dyadic n holds
F . x = (G . n) . x ) )
let A, B be closed Subset of T; ( A <> {} & A misses B implies for G being Rain of A,B ex F being Function of DOM,(bool the carrier of T) st
for x being Real st x in DOM holds
( ( x in halfline 0 implies F . x = {} ) & ( x in right_open_halfline 1 implies F . x = the carrier of T ) & ( x in DYADIC implies for n being Nat st x in dyadic n holds
F . x = (G . n) . x ) ) )
assume A1:
( A <> {} & A misses B )
; for G being Rain of A,B ex F being Function of DOM,(bool the carrier of T) st
for x being Real st x in DOM holds
( ( x in halfline 0 implies F . x = {} ) & ( x in right_open_halfline 1 implies F . x = the carrier of T ) & ( x in DYADIC implies for n being Nat st x in dyadic n holds
F . x = (G . n) . x ) )
let G be Rain of A,B; ex F being Function of DOM,(bool the carrier of T) st
for x being Real st x in DOM holds
( ( x in halfline 0 implies F . x = {} ) & ( x in right_open_halfline 1 implies F . x = the carrier of T ) & ( x in DYADIC implies for n being Nat st x in dyadic n holds
F . x = (G . n) . x ) )
defpred S1[ Element of DOM , set ] means ( ( $1 in halfline 0 implies $2 = {} ) & ( $1 in right_open_halfline 1 implies $2 = the carrier of T ) & ( $1 in DYADIC implies for n being Nat st $1 in dyadic n holds
$2 = (G . n) . $1 ) );
A2:
for x being Element of DOM ex y being Subset of T st S1[x,y]
ex F being Function of DOM,(bool the carrier of T) st
for x being Element of DOM holds S1[x,F . x]
from FUNCT_2:sch 3(A2);
then consider F being Function of DOM,(bool the carrier of T) such that
A17:
for x being Element of DOM holds S1[x,F . x]
;
take
F
; for x being Real st x in DOM holds
( ( x in halfline 0 implies F . x = {} ) & ( x in right_open_halfline 1 implies F . x = the carrier of T ) & ( x in DYADIC implies for n being Nat st x in dyadic n holds
F . x = (G . n) . x ) )
thus
for x being Real st x in DOM holds
( ( x in halfline 0 implies F . x = {} ) & ( x in right_open_halfline 1 implies F . x = the carrier of T ) & ( x in DYADIC implies for n being Nat st x in dyadic n holds
F . x = (G . n) . x ) )
by A17; verum