let i be Nat; :: thesis: for t being 1 _greater Nat holds (Partial_Union (Equal_Div_interval t)) . i = [.0,((i + 1) / t).[
let t be 1 _greater Nat; :: thesis: (Partial_Union (Equal_Div_interval t)) . i = [.0,((i + 1) / t).[
defpred S₁[ Nat] means (Partial_Union (Equal_Div_interval t)) . $1 = [.0,(($1 + 1) / t).[;
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: (Partial_Union (Equal_Div_interval t)) . k = [.0,((k + 1) / t).[ ; :: thesis: S₁[k + 1]
(Partial_Union (Equal_Div_interval t)) . (k + 1) = ((Partial_Union (Equal_Div_interval t)) . k) \/ ((Equal_Div_interval t) . (k + 1)) by PROB_3:def 2
.= [.0,((k + 1) / t).[ \/ [.((k + 1) / t),(((k + 1) / t) + (t ")).[ by Def1, A2
.= [.0,((k + 2) / t).[ by Lm2 ;
hence S₁[k + 1] ; :: thesis: verum

end;

(Partial_Union (Equal_Div_interval t)) . 0 = (Equal_Div_interval t) . 0 by PROB_3:def 2
.= [.(0 / t),((0 / t) + (t ")).[ by Def1
.= [.0,(t ").[ ;
then A3: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A1);
hence (Partial_Union (Equal_Div_interval t)) . i = [.0,((i + 1) / t).[ ; :: thesis: verum