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 Element of 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 Element of 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 Element of 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 Element of 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 Element of NAT holds (G . (inf_number_dyadic x)) . x = (G . ((inf_number_dyadic x) + n)) . x )
set s = inf_number_dyadic x;
defpred S₁[ Element of NAT ] means (G . (inf_number_dyadic x)) . x = (G . ((inf_number_dyadic x) + $1)) . x;
assume A2: x in DYADIC ; :: thesis: for n being Element of NAT holds (G . (inf_number_dyadic x)) . x = (G . ((inf_number_dyadic x) + n)) . x
A3: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: (G . (inf_number_dyadic x)) . x = (G . ((inf_number_dyadic x) + n)) . x ; :: thesis: S₁[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, Th7;
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, Th7, NAT_1:11;
hence S₁[n + 1] by A1, A4, A5, A6, Def2; :: thesis: verum

end;

A7: S₁[ 0 ] ;
for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A7, A3);
hence for n being Element of NAT holds (G . (inf_number_dyadic x)) . x = (G . ((inf_number_dyadic x) + n)) . x ; :: thesis: verum