let n be Element of NAT ; :: thesis: Sum (((1 / 2) GeoSeq) ^\ (n + 1)) = (1 / 2) |^ n
set r = 1 / 2;
thus Sum (((1 / 2) GeoSeq) ^\ (n + 1)) = ((1 / 2) |^ (n + 1)) / (1 - (1 / 2)) by Th22
.= (((1 / 2) |^ n) * (1 / 2)) / (1 / 2) by NEWTON:6
.= (1 / 2) |^ n ; :: thesis: verum