for k being Nat holds SumsReciTriang . k = ((seq_const 2) . k) + ((- (geo-seq (2,1))) . k)
proof
let k be Nat; :: thesis: SumsReciTriang . k = ((seq_const 2) . k) + ((- (geo-seq (2,1))) . k)
A1: SumsReciTriang . k = 2 - (2 / (k + 1)) by Def14;
A2: (seq_const 2) . k = 2 by SEQ_1:57;
- ((geo-seq (2,1)) . k) = (- (geo-seq (2,1))) . k by VALUED_1:8;
then (- (geo-seq (2,1))) . k = - (2 / (k + 1)) by Def15;
hence SumsReciTriang . k = ((seq_const 2) . k) + ((- (geo-seq (2,1))) . k) by A1, A2; :: thesis: verum
end;
hence SumsReciTriang = (seq_const 2) + (- (geo-seq (2,1))) by SEQ_1:7; :: thesis: verum