let T be non empty normal TopSpace; :: thesis: for A, B being closed Subset of T st A <> {} & A misses B holds

for G being Rain of A,B

for x being Real st x in DYADIC holds

for n being Nat holds (G . (inf_number_dyadic x)) . x = (G . ((inf_number_dyadic x) + n)) . x

let A, B be closed Subset of T; :: thesis: ( A <> {} & A misses B implies for G being Rain of A,B

for x being Real st x in DYADIC holds

for n being Nat holds (G . (inf_number_dyadic x)) . x = (G . ((inf_number_dyadic x) + n)) . x )

assume A1: ( A <> {} & A misses B ) ; :: thesis: for G being Rain of A,B

for x being Real st x in DYADIC holds

for n being Nat holds (G . (inf_number_dyadic x)) . x = (G . ((inf_number_dyadic x) + n)) . x

let G be Rain of A,B; :: thesis: for x being Real st x in DYADIC holds

for n being Nat holds (G . (inf_number_dyadic x)) . x = (G . ((inf_number_dyadic x) + n)) . x

let x be Real; :: thesis: ( x in DYADIC implies for n being Nat holds (G . (inf_number_dyadic x)) . x = (G . ((inf_number_dyadic x) + n)) . x )

set s = inf_number_dyadic x;

defpred S_{1}[ Nat] means (G . (inf_number_dyadic x)) . x = (G . ((inf_number_dyadic x) + $1)) . x;

assume A2: x in DYADIC ; :: thesis: for n being Nat holds (G . (inf_number_dyadic x)) . x = (G . ((inf_number_dyadic x) + n)) . x

A3: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[ 0 ]
;

for i being Nat holds S_{1}[i]
from NAT_1:sch 2(A7, A3);

hence for n being Nat holds (G . (inf_number_dyadic x)) . x = (G . ((inf_number_dyadic x) + n)) . x ; :: thesis: verum

for G being Rain of A,B

for x being Real st x in DYADIC holds

for n being Nat holds (G . (inf_number_dyadic x)) . x = (G . ((inf_number_dyadic x) + n)) . x

let A, B be closed Subset of T; :: thesis: ( A <> {} & A misses B implies for G being Rain of A,B

for x being Real st x in DYADIC holds

for n being Nat holds (G . (inf_number_dyadic x)) . x = (G . ((inf_number_dyadic x) + n)) . x )

assume A1: ( A <> {} & A misses B ) ; :: thesis: for G being Rain of A,B

for x being Real st x in DYADIC holds

for n being Nat holds (G . (inf_number_dyadic x)) . x = (G . ((inf_number_dyadic x) + n)) . x

let G be Rain of A,B; :: thesis: for x being Real st x in DYADIC holds

for n being Nat holds (G . (inf_number_dyadic x)) . x = (G . ((inf_number_dyadic x) + n)) . x

let x be Real; :: thesis: ( x in DYADIC implies for n being Nat holds (G . (inf_number_dyadic x)) . x = (G . ((inf_number_dyadic x) + n)) . x )

set s = inf_number_dyadic x;

defpred S

assume A2: x in DYADIC ; :: thesis: for n being Nat holds (G . (inf_number_dyadic x)) . x = (G . ((inf_number_dyadic x) + n)) . x

A3: for n being Nat st S

S

proof

A7:
S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A4: (G . (inf_number_dyadic x)) . x = (G . ((inf_number_dyadic x) + n)) . x ; :: thesis: S_{1}[n + 1]

inf_number_dyadic x <= (inf_number_dyadic x) + (n + 1) by NAT_1:11;

then A5: x in dyadic (((inf_number_dyadic x) + n) + 1) by A2, Th6;

G . ((inf_number_dyadic x) + n) is Drizzle of A,B,(inf_number_dyadic x) + n by A1, Def2;

then A6: dom (G . ((inf_number_dyadic x) + n)) = dyadic ((inf_number_dyadic x) + n) by FUNCT_2:def 1;

x in dyadic ((inf_number_dyadic x) + n) by A2, Th6, NAT_1:11;

hence S_{1}[n + 1]
by A1, A4, A5, A6, Def2; :: thesis: verum

end;assume A4: (G . (inf_number_dyadic x)) . x = (G . ((inf_number_dyadic x) + n)) . x ; :: thesis: S

inf_number_dyadic x <= (inf_number_dyadic x) + (n + 1) by NAT_1:11;

then A5: x in dyadic (((inf_number_dyadic x) + n) + 1) by A2, Th6;

G . ((inf_number_dyadic x) + n) is Drizzle of A,B,(inf_number_dyadic x) + n by A1, Def2;

then A6: dom (G . ((inf_number_dyadic x) + n)) = dyadic ((inf_number_dyadic x) + n) by FUNCT_2:def 1;

x in dyadic ((inf_number_dyadic x) + n) by A2, Th6, NAT_1:11;

hence S

for i being Nat holds S

hence for n being Nat holds (G . (inf_number_dyadic x)) . x = (G . ((inf_number_dyadic x) + n)) . x ; :: thesis: verum