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 ")).[ \/ (halfline_fin (((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
.= halfline_fin ((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