let A be closed-interval Subset of REAL ; :: thesis: for Z being open Subset of REAL
for f being PartFunc of REAL ,REAL st A c= Z & f = #Z 2 & Z = dom ((1 / 2) (#) f) holds
integral (id Z),A = (((1 / 2) (#) f) . (sup A)) - (((1 / 2) (#) f) . (inf A))
let Z be open Subset of REAL ; :: thesis: for f being PartFunc of REAL ,REAL st A c= Z & f = #Z 2 & Z = dom ((1 / 2) (#) f) holds
integral (id Z),A = (((1 / 2) (#) f) . (sup A)) - (((1 / 2) (#) f) . (inf A))
let f be PartFunc of REAL ,REAL ; :: thesis: ( A c= Z & f = #Z 2 & Z = dom ((1 / 2) (#) f) implies integral (id Z),A = (((1 / 2) (#) f) . (sup A)) - (((1 / 2) (#) f) . (inf A)) )
assume A1: ( A c= Z & f = #Z 2 & Z = dom ((1 / 2) (#) f) ) ; :: thesis: integral (id Z),A = (((1 / 2) (#) f) . (sup A)) - (((1 / 2) (#) f) . (inf A))
AA: (id Z) | A is continuous ;
A c= dom (id Z) by A1, FUNCT_1:34;
then A2: ( id Z is_integrable_on A & (id Z) | A is bounded ) by AA, INTEGRA5:10, INTEGRA5:11;
B1: dom (id Z) = Z by FUNCT_1:34;
A3: (1 / 2) (#) f is_differentiable_on Z by A1, Th1;
A4: for x being Real st x in dom (((1 / 2) (#) f) `| Z) holds
(((1 / 2) (#) f) `| Z) . x = (id Z) . x

proof

let x be Real; :: thesis: ( x in dom (((1 / 2) (#) f) `| Z) implies (((1 / 2) (#) f) `| Z) . x = (id Z) . x )
assume x in dom (((1 / 2) (#) f) `| Z) ; :: thesis: (((1 / 2) (#) f) `| Z) . x = (id Z) . x
then A5: x in Z by A3, FDIFF_1:def 8;
then (((1 / 2) (#) f) `| Z) . x = x by A1, Th1
.= (id Z) . x by A5, FUNCT_1:35 ;
hence (((1 / 2) (#) f) `| Z) . x = (id Z) . x ; :: thesis: verum

end;

dom (((1 / 2) (#) f) `| Z) = dom (id Z) by B1, A3, FDIFF_1:def 8;
then ((1 / 2) (#) f) `| Z = id Z by A4, PARTFUN1:34;
hence integral (id Z),A = (((1 / 2) (#) f) . (sup A)) - (((1 / 2) (#) f) . (inf A)) by A1, A2, Th1, INTEGRA5:13; :: thesis: verum