let x, y be PartFunc of REAL,REAL; :: thesis: for Z being open Subset of REAL
for G being Real_Sequence st integral ((y (#) (x `| Z)),0,PI) <= ((1 / 2) * PI) - ((1 / 2) * (lim G)) & 0 <= lim G & ((1 / 2) * PI) - ((1 / 2) * (lim G)) <= (1 / 2) * PI & integral ((y (#) (x `| Z)),0,PI) = (1 / 2) * PI holds
lim G = 0
let Z be open Subset of REAL; :: thesis: for G being Real_Sequence st integral ((y (#) (x `| Z)),0,PI) <= ((1 / 2) * PI) - ((1 / 2) * (lim G)) & 0 <= lim G & ((1 / 2) * PI) - ((1 / 2) * (lim G)) <= (1 / 2) * PI & integral ((y (#) (x `| Z)),0,PI) = (1 / 2) * PI holds
lim G = 0
let G be Real_Sequence; :: thesis: ( integral ((y (#) (x `| Z)),0,PI) <= ((1 / 2) * PI) - ((1 / 2) * (lim G)) & 0 <= lim G & ((1 / 2) * PI) - ((1 / 2) * (lim G)) <= (1 / 2) * PI & integral ((y (#) (x `| Z)),0,PI) = (1 / 2) * PI implies lim G = 0 )
assume A1: ( integral ((y (#) (x `| Z)),0,PI) <= ((1 / 2) * PI) - ((1 / 2) * (lim G)) & 0 <= lim G & ((1 / 2) * PI) - ((1 / 2) * (lim G)) <= (1 / 2) * PI ) ; :: thesis: ( not integral ((y (#) (x `| Z)),0,PI) = (1 / 2) * PI or lim G = 0 )
assume integral ((y (#) (x `| Z)),0,PI) = (1 / 2) * PI ; :: thesis: lim G = 0
then (1 / 2) * PI = ((1 / 2) * PI) - ((1 / 2) * (lim G)) by A1, XXREAL_0:1;
hence lim G = 0 ; :: thesis: verum