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 )
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
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;
A3: S₁[ 0 ] ;
A4: 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 A5: (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 & inf_number_dyadic x <= (inf_number_dyadic x) + (n + 1) ) by NAT_1:11;
then A6: ( x in dyadic ((inf_number_dyadic x) + n) & 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 & ( for r being Element of dom (G . ((inf_number_dyadic x) + n)) holds (G . ((inf_number_dyadic x) + n)) . r = (G . (((inf_number_dyadic x) + n) + 1)) . r ) ) by A1, Def2;
then dom (G . ((inf_number_dyadic x) + n)) = dyadic ((inf_number_dyadic x) + n) by FUNCT_2:def 1;
hence S₁[n + 1] by A1, A5, A6, Def2; :: thesis: verum

end;

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