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 . ) . x = (G . ( + 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 . ) . x = (G . ( + 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 . ) . x = (G . ( + 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 . ) . x = (G . ( + n)) . x

let x be Real; :: thesis: ( x in DYADIC implies for n being Nat holds (G . ) . x = (G . ( + n)) . x )
defpred S1[ Nat] means (G . ) . x = (G . ( + \$1)) . x;
assume A2: x in DYADIC ; :: thesis: for n being Nat holds (G . ) . x = (G . ( + n)) . x
A3: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A4: (G . ) . x = (G . ( + n)) . x ; :: thesis: S1[n + 1]
inf_number_dyadic x <= + (n + 1) by NAT_1:11;
then A5: x in dyadic (( + n) + 1) by ;
G . ( + n) is Drizzle of A,B, + n by ;
then A6: dom (G . ( + n)) = dyadic ( + n) by FUNCT_2:def 1;
x in dyadic ( + n) by ;
hence S1[n + 1] by A1, A4, A5, A6, Def2; :: thesis: verum
end;
A7: S1[ 0 ] ;
for i being Nat holds S1[i] from NAT_1:sch 2(A7, A3);
hence for n being Nat holds (G . ) . x = (G . ( + n)) . x ; :: thesis: verum