let a, b be Real; :: thesis: for f, F being PartFunc of REAL,REAL st a <= b & [.a,b.] c= dom f & f | ['a,b'] is bounded & f is_integrable_on ['a,b'] & [.a,b.] = dom F & ( for x being Real st x in [.a,b.] holds
F . x = integral (f,a,x) ) holds
F is Lipschitzian
let f, F be PartFunc of REAL,REAL; :: thesis: ( a <= b & [.a,b.] c= dom f & f | ['a,b'] is bounded & f is_integrable_on ['a,b'] & [.a,b.] = dom F & ( for x being Real st x in [.a,b.] holds
F . x = integral (f,a,x) ) implies F is Lipschitzian )
assume that
A1: a <= b and
A2: [.a,b.] c= dom f and
A3: f | ['a,b'] is bounded and
A4: f is_integrable_on ['a,b'] and
A5: [.a,b.] = dom F and
A6: for x being Real st x in [.a,b.] holds
F . x = integral (f,a,x) ; :: thesis: F is Lipschitzian
A7: [.a,b.] = ['a,b'] by A1, INTEGRA5:def 3;
consider r0 being Real such that
A8: for x being object st x in ['a,b'] /\ (dom f) holds
|.(f . x).| <= r0 by A3, RFUNCT_1:73;
reconsider r = max (r0,1) as Real ;
A9: 0 < r by XXREAL_0:25;
A10: r0 <= r by XXREAL_0:25;
A11: for p, q being Real st p in [.a,b.] & q in [.a,b.] & p <= q holds
( f is_integrable_on ['p,q'] & f | ['p,q'] is bounded )

proof

let p, q be Real; :: thesis: ( p in [.a,b.] & q in [.a,b.] & p <= q implies ( f is_integrable_on ['p,q'] & f | ['p,q'] is bounded ) )
assume A12: ( p in [.a,b.] & q in [.a,b.] & p <= q ) ; :: thesis: ( f is_integrable_on ['p,q'] & f | ['p,q'] is bounded )
( a <= p & q <= b ) by A12, XXREAL_1:1;
hence ( f is_integrable_on ['p,q'] & f | ['p,q'] is bounded ) by A2, A3, A4, A7, A12, INTEGRA6:18; :: thesis: verum

end;

for x1, x2 being Real st x1 in dom F & x2 in dom F holds
|.((F . x1) - (F . x2)).| <= r * |.(x1 - x2).|

proof

let x1, x2 be Real; :: thesis: ( x1 in dom F & x2 in dom F implies |.((F . x1) - (F . x2)).| <= r * |.(x1 - x2).| )
assume A13: ( x1 in dom F & x2 in dom F ) ; :: thesis: |.((F . x1) - (F . x2)).| <= r * |.(x1 - x2).|
then ( F . x1 = integral (f,a,x1) & F . x2 = integral (f,a,x2) ) by A5, A6;
then A14: F . x1 = (F . x2) + (integral (f,x2,x1)) by A1, A4, A3, A2, A5, A7, A13, INTEGRA6:20;

per cases ( x1 <= x2 or x2 <= x1 ) ;

suppose A15: x1 <= x2 ; :: thesis: |.((F . x1) - (F . x2)).| <= r * |.(x1 - x2).|

then A16: ( f is_integrable_on ['x1,x2'] & f | ['x1,x2'] is bounded ) by A5, A13, A11;
A17: [.x1,x2.] = ['x1,x2'] by A15, INTEGRA5:def 3;
A18: ['x1,x2'] c= [.a,b.] by A17, A5, A13, XXREAL_2:def 12;
then A19: ['x1,x2'] c= dom f by A2;
A20: ( x1 in ['x1,x2'] & x2 in ['x1,x2'] ) by A15, A17, XXREAL_1:1;
for x being Real st x in ['x1,x2'] holds
|.(f . x).| <= r

proof

let x be Real; :: thesis: ( x in ['x1,x2'] implies |.(f . x).| <= r )
assume x in ['x1,x2'] ; :: thesis: |.(f . x).| <= r
then x in [.a,b.] /\ (dom f) by A18, A19, XBOOLE_0:def 4;
then |.(f . x).| <= r0 by A8, A7;
hence |.(f . x).| <= r by A10, XXREAL_0:2; :: thesis: verum

end;

then |.((F . x1) - (F . x2)).| <= r * (x2 - x1) by A14, A15, A16, A19, A20, INTEGRA6:23;
then |.((F . x1) - (F . x2)).| <= r * |.(x2 - x1).| by A15, XREAL_1:48, COMPLEX1:43;
hence |.((F . x1) - (F . x2)).| <= r * |.(x1 - x2).| by COMPLEX1:60; :: thesis: verum

end;

suppose A21: x2 <= x1 ; :: thesis: |.((F . x1) - (F . x2)).| <= r * |.(x1 - x2).|

then A22: ( f is_integrable_on ['x2,x1'] & f | ['x2,x1'] is bounded ) by A5, A13, A11;
A23: [.x2,x1.] = ['x2,x1'] by A21, INTEGRA5:def 3;
A24: ['x2,x1'] c= [.a,b.] by A23, A5, A13, XXREAL_2:def 12;
then A25: ['x2,x1'] c= dom f by A2;
A26: ( x1 in ['x2,x1'] & x2 in ['x2,x1'] ) by A21, A23, XXREAL_1:1;
for x being Real st x in ['x2,x1'] holds
|.(f . x).| <= r

proof

let x be Real; :: thesis: ( x in ['x2,x1'] implies |.(f . x).| <= r )
assume x in ['x2,x1'] ; :: thesis: |.(f . x).| <= r
then x in [.a,b.] /\ (dom f) by A24, A25, XBOOLE_0:def 4;
then |.(f . x).| <= r0 by A8, A7;
hence |.(f . x).| <= r by A10, XXREAL_0:2; :: thesis: verum

end;

then |.((F . x1) - (F . x2)).| <= r * (x1 - x2) by A14, A21, A22, A25, A26, INTEGRA6:23;
hence |.((F . x1) - (F . x2)).| <= r * |.(x1 - x2).| by A21, XREAL_1:48, COMPLEX1:43; :: thesis: verum

end;

end;

end;

hence F is Lipschitzian by A9, FCONT_1:def 3; :: thesis: verum