let X be set ; :: thesis: for n being Element of NAT holds Sum ((X -powers (1 / 2)) ^\ (n + 1)) <= (1 / 2) |^ n
let n be Element of NAT ; :: thesis: Sum ((X -powers (1 / 2)) ^\ (n + 1)) <= (1 / 2) |^ n
set r = 1 / 2;
|.(1 / 2).| = 1 / 2 by ABSVALUE:def 1;
then A1: ((1 / 2) GeoSeq) ^\ (n + 1) is summable by SERIES_1:12, SERIES_1:24;

A2: now :: thesis: for m being Nat holds
( 0 <= ((X -powers (1 / 2)) ^\ (n + 1)) . m & ((X -powers (1 / 2)) ^\ (n + 1)) . m <= (((1 / 2) GeoSeq) ^\ (n + 1)) . m )

let m be Nat; :: thesis: ( 0 <= ((X -powers (1 / 2)) ^\ (n + 1)) . m & ((X -powers (1 / 2)) ^\ (n + 1)) . m <= (((1 / 2) GeoSeq) ^\ (n + 1)) . m )
A3: ((X -powers (1 / 2)) ^\ (n + 1)) . m = (X -powers (1 / 2)) . (m + (n + 1)) by NAT_1:def 3;
A4: ( ( m + (n + 1) in X & (X -powers (1 / 2)) . (m + (n + 1)) = (1 / 2) |^ (m + (n + 1)) ) or ( not m + (n + 1) in X & (X -powers (1 / 2)) . (m + (n + 1)) = 0 ) ) by Def5;
hence 0 <= ((X -powers (1 / 2)) ^\ (n + 1)) . m by A3, PREPOWER:6; :: thesis: ((X -powers (1 / 2)) ^\ (n + 1)) . m <= (((1 / 2) GeoSeq) ^\ (n + 1)) . m
A5: ((1 / 2) GeoSeq) . (m + (n + 1)) = (1 / 2) |^ (m + (n + 1)) by PREPOWER:def 1;
(((1 / 2) GeoSeq) ^\ (n + 1)) . m = ((1 / 2) GeoSeq) . (m + (n + 1)) by NAT_1:def 3;
hence ((X -powers (1 / 2)) ^\ (n + 1)) . m <= (((1 / 2) GeoSeq) ^\ (n + 1)) . m by A5, A3, A4, PREPOWER:6; :: thesis: verum

end;

Sum (((1 / 2) GeoSeq) ^\ (n + 1)) = (1 / 2) |^ n by Th23;
hence Sum ((X -powers (1 / 2)) ^\ (n + 1)) <= (1 / 2) |^ n by A1, A2, SERIES_1:20; :: thesis: verum