let A be non empty closed_interval Subset of REAL; :: thesis: for r being Real
for f being FuzzySet of REAL
for F being Function of REAL,REAL st r > 0 & f is_integrable_on A & f | A is bounded & ( for x being Real holds F . x = min (r,(f . x)) ) holds
integral (F,A) >= 0
let r be Real; :: thesis: for f being FuzzySet of REAL
for F being Function of REAL,REAL st r > 0 & f is_integrable_on A & f | A is bounded & ( for x being Real holds F . x = min (r,(f . x)) ) holds
integral (F,A) >= 0
let f be FuzzySet of REAL; :: thesis: for F being Function of REAL,REAL st r > 0 & f is_integrable_on A & f | A is bounded & ( for x being Real holds F . x = min (r,(f . x)) ) holds
integral (F,A) >= 0
let F be Function of REAL,REAL; :: thesis: ( r > 0 & f is_integrable_on A & f | A is bounded & ( for x being Real holds F . x = min (r,(f . x)) ) implies integral (F,A) >= 0 )
assume that
A1: r > 0 and
A2: ( f is_integrable_on A & f | A is bounded ) and
A4: for x being Real holds F . x = min (r,(f . x)) ; :: thesis: integral (F,A) >= 0
ex r being Real st
for y being set st y in dom (F | A) holds
|.((F | A) . y).| < r

proof

consider e being Real such that
C1: for y being set st y in dom (f | A) holds
|.((f | A) . y).| < e by COMSEQ_2:def 3, A2;
take (max (r,e)) + 1 ; :: thesis: for y being set st y in dom (F | A) holds
|.((F | A) . y).| < (max (r,e)) + 1
M1: (max (r,e)) + 0 < (max (r,e)) + 1 by XREAL_1:8;
for y being set st y in dom (F | A) holds
|.((F | A) . y).| < (max (r,e)) + 1

proof

let x be set ; :: thesis: ( x in dom (F | A) implies |.((F | A) . x).| < (max (r,e)) + 1 )
assume B1: x in dom (F | A) ; :: thesis: |.((F | A) . x).| < (max (r,e)) + 1
B3a: dom (f | A) = A by FUNCT_2:def 1;
reconsider x = x as Real by B1;

per cases ( min (r,(f . x)) = r or min (r,(f . x)) = f . x ) by XXREAL_0:15;

suppose D1: min (r,(f . x)) = r ; :: thesis: |.((F | A) . x).| < (max (r,e)) + 1

|.((F | A) . x).| = |.(F . x).| by FUNCT_1:49, B1
.= |.r.| by D1, A4
.= r by A1, ABSVALUE:def 1 ;
then |.((F | A) . x).| <= max (r,e) by XXREAL_0:25;
hence |.((F | A) . x).| < (max (r,e)) + 1 by M1, XXREAL_0:2; :: thesis: verum

end;

suppose D2: min (r,(f . x)) = f . x ; :: thesis: |.((F | A) . x).| < (max (r,e)) + 1

B44: |.((F | A) . x).| = |.(F . x).| by FUNCT_1:49, B1
.= |.(f . x).| by D2, A4
.= |.((f | A) . x).| by FUNCT_1:49, B1 ;
e <= max (r,e) by XXREAL_0:25;
then |.((F | A) . x).| < max (r,e) by XXREAL_0:2, C1, B3a, B1, B44;
hence |.((F | A) . x).| < (max (r,e)) + 1 by XXREAL_0:2, M1; :: thesis: verum

end;

end;

end;

hence for y being set st y in dom (F | A) holds
|.((F | A) . y).| < (max (r,e)) + 1 ; :: thesis: verum

end;

then A5: (F | A) | A is bounded by COMSEQ_2:def 3;
for x being Real st x in A holds
0 <= (F | A) . x

proof

let x be Real; :: thesis: ( x in A implies 0 <= (F | A) . x )
assume C2: x in A ; :: thesis: 0 <= (F | A) . x

per cases ( min (r,(f . x)) = r or min (r,(f . x)) = f . x ) by XXREAL_0:15;

suppose D3: min (r,(f . x)) = r ; :: thesis: 0 <= (F | A) . x

(F | A) . x = F . x by FUNCT_1:49, C2
.= r by D3, A4 ;
hence 0 <= (F | A) . x by A1; :: thesis: verum

end;

suppose D4: min (r,(f . x)) = f . x ; :: thesis: 0 <= (F | A) . x

reconsider x = x as Element of REAL by C2;
(F | A) . x = F . x by FUNCT_1:49, C2
.= f . x by D4, A4 ;
hence 0 <= (F | A) . x by FUZZY_2:1; :: thesis: verum

end;

end;

end;

then 0 <= integral (F | A) by A5, INTEGRA2:32;
hence 0 <= integral (F,A) by INTEGRA5:def 2; :: thesis: verum