let f be PartFunc of COMPLEX,COMPLEX; :: thesis: for C being C1-curve st rng C c= dom f & f is_integrable_on C & f is_bounded_on C holds
for r being Real holds integral ((r (#) f),C) = r * (integral (f,C))
let C be C1-curve; :: thesis: ( rng C c= dom f & f is_integrable_on C & f is_bounded_on C implies for r being Real holds integral ((r (#) f),C) = r * (integral (f,C)) )
assume A1: ( rng C c= dom f & f is_integrable_on C & f is_bounded_on C ) ; :: thesis: for r being Real holds integral ((r (#) f),C) = r * (integral (f,C))
let r be Real; :: thesis: integral ((r (#) f),C) = r * (integral (f,C))
consider a, b being Real, x, y being PartFunc of REAL,REAL, Z being Subset of REAL such that
A2: ( a <= b & [.a,b.] = dom C & [.a,b.] c= dom x & [.a,b.] c= dom y & Z is open & [.a,b.] c= Z & x is_differentiable_on Z & y is_differentiable_on Z & x `| Z is continuous & y `| Z is continuous & C = (x + (<i> (#) y)) | [.a,b.] ) by Def3;
reconsider a = a, b = b as Real ;
consider uf0, vf0 being PartFunc of REAL,REAL such that
A3: ( uf0 = ((Re f) * R2-to-C) * <:x,y:> & vf0 = ((Im f) * R2-to-C) * <:x,y:> & integral (f,x,y,a,b,Z) = (integral (((uf0 (#) (x `| Z)) - (vf0 (#) (y `| Z))),a,b)) + ((integral (((vf0 (#) (x `| Z)) + (uf0 (#) (y `| Z))),a,b)) * <i>) ) by Def2;
A4: dom (r (#) f) = dom f by VALUED_1:def 5;
consider u0, v0 being PartFunc of REAL,REAL such that
A5: ( u0 = ((Re (r (#) f)) * R2-to-C) * <:x,y:> & v0 = ((Im (r (#) f)) * R2-to-C) * <:x,y:> & integral ((r (#) f),x,y,a,b,Z) = (integral (((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))),a,b)) + ((integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),a,b)) * <i>) ) by Def2;
A6: dom u0 = dom uf0

proof

A7: for x0 being object st x0 in dom u0 holds
x0 in dom uf0

proof

let x0 be object ; :: thesis: ( x0 in dom u0 implies x0 in dom uf0 )
assume A8: x0 in dom u0 ; :: thesis: x0 in dom uf0
A9: ( x0 in dom <:x,y:> & <:x,y:> . x0 in dom ((Re (r (#) f)) * R2-to-C) ) by A5, A8, FUNCT_1:11;
set R2 = <:x,y:> . x0;
A10: ( <:x,y:> . x0 in dom R2-to-C & R2-to-C . (<:x,y:> . x0) in dom (Re (r (#) f)) ) by A9, FUNCT_1:11;
then R2-to-C . (<:x,y:> . x0) in dom (r (#) (Re f)) by MESFUN6C:2;
then R2-to-C . (<:x,y:> . x0) in dom (Re f) by VALUED_1:def 5;
then <:x,y:> . x0 in dom ((Re f) * R2-to-C) by A10, FUNCT_1:11;
hence x0 in dom uf0 by A3, A9, FUNCT_1:11; :: thesis: verum

end;

for x0 being object st x0 in dom uf0 holds
x0 in dom u0

proof

let x0 be object ; :: thesis: ( x0 in dom uf0 implies x0 in dom u0 )
assume A11: x0 in dom uf0 ; :: thesis: x0 in dom u0
A12: ( x0 in dom <:x,y:> & <:x,y:> . x0 in dom ((Re f) * R2-to-C) ) by A3, A11, FUNCT_1:11;
set R2 = <:x,y:> . x0;
A13: ( <:x,y:> . x0 in dom R2-to-C & R2-to-C . (<:x,y:> . x0) in dom (Re f) ) by A12, FUNCT_1:11;
then R2-to-C . (<:x,y:> . x0) in dom (r (#) (Re f)) by VALUED_1:def 5;
then R2-to-C . (<:x,y:> . x0) in dom (Re (r (#) f)) by MESFUN6C:2;
then <:x,y:> . x0 in dom ((Re (r (#) f)) * R2-to-C) by A13, FUNCT_1:11;
hence x0 in dom u0 by A5, A12, FUNCT_1:11; :: thesis: verum

end;

hence dom u0 = dom uf0 by A7, TARSKI:2; :: thesis: verum

end;

A14: dom v0 = dom vf0

proof

A15: for x0 being object st x0 in dom v0 holds
x0 in dom vf0

proof

let x0 be object ; :: thesis: ( x0 in dom v0 implies x0 in dom vf0 )
assume A16: x0 in dom v0 ; :: thesis: x0 in dom vf0
A17: ( x0 in dom <:x,y:> & <:x,y:> . x0 in dom ((Im (r (#) f)) * R2-to-C) ) by A16, A5, FUNCT_1:11;
set R2 = <:x,y:> . x0;
A18: ( <:x,y:> . x0 in dom R2-to-C & R2-to-C . (<:x,y:> . x0) in dom (Im (r (#) f)) ) by A17, FUNCT_1:11;
then R2-to-C . (<:x,y:> . x0) in dom (r (#) (Im f)) by MESFUN6C:2;
then R2-to-C . (<:x,y:> . x0) in dom (Im f) by VALUED_1:def 5;
then <:x,y:> . x0 in dom ((Im f) * R2-to-C) by A18, FUNCT_1:11;
hence x0 in dom vf0 by A3, A17, FUNCT_1:11; :: thesis: verum

end;

for x0 being object st x0 in dom vf0 holds
x0 in dom v0

proof

let x0 be object ; :: thesis: ( x0 in dom vf0 implies x0 in dom v0 )
assume A19: x0 in dom vf0 ; :: thesis: x0 in dom v0
A20: ( x0 in dom <:x,y:> & <:x,y:> . x0 in dom ((Im f) * R2-to-C) ) by A19, A3, FUNCT_1:11;
set R2 = <:x,y:> . x0;
A21: ( <:x,y:> . x0 in dom R2-to-C & R2-to-C . (<:x,y:> . x0) in dom (Im f) ) by A20, FUNCT_1:11;
then R2-to-C . (<:x,y:> . x0) in dom (r (#) (Im f)) by VALUED_1:def 5;
then R2-to-C . (<:x,y:> . x0) in dom (Im (r (#) f)) by MESFUN6C:2;
then <:x,y:> . x0 in dom ((Im (r (#) f)) * R2-to-C) by A21, FUNCT_1:11;
hence x0 in dom v0 by A5, A20, FUNCT_1:11; :: thesis: verum

end;

hence dom v0 = dom vf0 by A15, TARSKI:2; :: thesis: verum

end;

A22: u0 (#) (x `| Z) = r (#) (uf0 (#) (x `| Z))

proof

A23: dom (r (#) (uf0 (#) (x `| Z))) = dom (uf0 (#) (r (#) (x `| Z))) by RFUNCT_1:13
.= (dom uf0) /\ (dom (r (#) (x `| Z))) by VALUED_1:def 4
.= (dom uf0) /\ (dom (x `| Z)) by VALUED_1:def 5 ;
A24: dom (u0 (#) (x `| Z)) = (dom u0) /\ (dom (x `| Z)) by VALUED_1:def 4;
A25: dom (u0 (#) (x `| Z)) = dom (r (#) (uf0 (#) (x `| Z))) by A6, A23, VALUED_1:def 4;
for x0 being object st x0 in dom (u0 (#) (x `| Z)) holds
(u0 (#) (x `| Z)) . x0 = (r (#) (uf0 (#) (x `| Z))) . x0

proof

let x0 be object ; :: thesis: ( x0 in dom (u0 (#) (x `| Z)) implies (u0 (#) (x `| Z)) . x0 = (r (#) (uf0 (#) (x `| Z))) . x0 )
assume A26: x0 in dom (u0 (#) (x `| Z)) ; :: thesis: (u0 (#) (x `| Z)) . x0 = (r (#) (uf0 (#) (x `| Z))) . x0
A27: x0 in (dom u0) /\ (dom (x `| Z)) by A26, VALUED_1:def 4;
then A28: ( x0 in dom u0 & x0 in dom (x `| Z) ) by XBOOLE_0:def 4;
then A29: ( x0 in dom <:x,y:> & <:x,y:> . x0 in dom ((Re (r (#) f)) * R2-to-C) ) by A5, FUNCT_1:11;
set R2 = <:x,y:> . x0;
set c0 = R2-to-C . (<:x,y:> . x0);
A30: u0 . x0 = ((Re (r (#) f)) * R2-to-C) . (<:x,y:> . x0) by A5, A28, FUNCT_1:12
.= (Re (r (#) f)) . (R2-to-C . (<:x,y:> . x0)) by A29, FUNCT_1:12
.= (r (#) (Re f)) . (R2-to-C . (<:x,y:> . x0)) by MESFUN6C:2 ;
x0 in dom uf0 by A6, A27, XBOOLE_0:def 4;
then A31: ( x0 in dom <:x,y:> & <:x,y:> . x0 in dom ((Re f) * R2-to-C) ) by A3, FUNCT_1:11;
A32: uf0 . x0 = ((Re f) * R2-to-C) . (<:x,y:> . x0) by A3, A6, A28, FUNCT_1:12
.= (Re f) . (R2-to-C . (<:x,y:> . x0)) by A31, FUNCT_1:12 ;
A33: x0 in dom (uf0 (#) (r (#) (x `| Z))) by A26, A25, RFUNCT_1:13;
then x0 in (dom uf0) /\ (dom (r (#) (x `| Z))) by VALUED_1:def 4;
then A34: x0 in dom (r (#) (x `| Z)) by XBOOLE_0:def 4;
(u0 (#) (x `| Z)) . x0 = (u0 . x0) * ((x `| Z) . x0) by A26, VALUED_1:def 4
.= (r * ((Re f) . (R2-to-C . (<:x,y:> . x0)))) * ((x `| Z) . x0) by A30, VALUED_1:6
.= (uf0 . x0) * (r * ((x `| Z) . x0)) by A32
.= (uf0 . x0) * ((r (#) (x `| Z)) . x0) by A34, VALUED_1:def 5
.= (uf0 (#) (r (#) (x `| Z))) . x0 by A33, VALUED_1:def 4
.= (r (#) (uf0 (#) (x `| Z))) . x0 by RFUNCT_1:13 ;
hence (u0 (#) (x `| Z)) . x0 = (r (#) (uf0 (#) (x `| Z))) . x0 ; :: thesis: verum

end;

hence u0 (#) (x `| Z) = r (#) (uf0 (#) (x `| Z)) by A6, A23, A24, FUNCT_1:2; :: thesis: verum

end;

A35: v0 (#) (x `| Z) = r (#) (vf0 (#) (x `| Z))

proof

A36: dom (r (#) (vf0 (#) (x `| Z))) = dom (vf0 (#) (r (#) (x `| Z))) by RFUNCT_1:13
.= (dom vf0) /\ (dom (r (#) (x `| Z))) by VALUED_1:def 4
.= (dom vf0) /\ (dom (x `| Z)) by VALUED_1:def 5 ;
A37: dom (v0 (#) (x `| Z)) = (dom v0) /\ (dom (x `| Z)) by VALUED_1:def 4;
A38: dom (v0 (#) (x `| Z)) = dom (r (#) (vf0 (#) (x `| Z))) by A14, A36, VALUED_1:def 4;
for x0 being object st x0 in dom (v0 (#) (x `| Z)) holds
(v0 (#) (x `| Z)) . x0 = (r (#) (vf0 (#) (x `| Z))) . x0

proof

let x0 be object ; :: thesis: ( x0 in dom (v0 (#) (x `| Z)) implies (v0 (#) (x `| Z)) . x0 = (r (#) (vf0 (#) (x `| Z))) . x0 )
assume A39: x0 in dom (v0 (#) (x `| Z)) ; :: thesis: (v0 (#) (x `| Z)) . x0 = (r (#) (vf0 (#) (x `| Z))) . x0
A40: x0 in (dom v0) /\ (dom (x `| Z)) by A39, VALUED_1:def 4;
then A41: ( x0 in dom v0 & x0 in dom (x `| Z) ) by XBOOLE_0:def 4;
then A42: ( x0 in dom <:x,y:> & <:x,y:> . x0 in dom ((Im (r (#) f)) * R2-to-C) ) by A5, FUNCT_1:11;
set R2 = <:x,y:> . x0;
set c0 = R2-to-C . (<:x,y:> . x0);
A43: v0 . x0 = ((Im (r (#) f)) * R2-to-C) . (<:x,y:> . x0) by A5, A41, FUNCT_1:12
.= (Im (r (#) f)) . (R2-to-C . (<:x,y:> . x0)) by A42, FUNCT_1:12
.= (r (#) (Im f)) . (R2-to-C . (<:x,y:> . x0)) by MESFUN6C:2 ;
x0 in dom vf0 by A14, A40, XBOOLE_0:def 4;
then A44: ( x0 in dom <:x,y:> & <:x,y:> . x0 in dom ((Im f) * R2-to-C) ) by A3, FUNCT_1:11;
A45: vf0 . x0 = ((Im f) * R2-to-C) . (<:x,y:> . x0) by A3, A14, A41, FUNCT_1:12
.= (Im f) . (R2-to-C . (<:x,y:> . x0)) by A44, FUNCT_1:12 ;
A46: x0 in dom (vf0 (#) (r (#) (x `| Z))) by A38, A39, RFUNCT_1:13;
then x0 in (dom vf0) /\ (dom (r (#) (x `| Z))) by VALUED_1:def 4;
then A47: x0 in dom (r (#) (x `| Z)) by XBOOLE_0:def 4;
(v0 (#) (x `| Z)) . x0 = (v0 . x0) * ((x `| Z) . x0) by A39, VALUED_1:def 4
.= (r * ((Im f) . (R2-to-C . (<:x,y:> . x0)))) * ((x `| Z) . x0) by A43, VALUED_1:6
.= (vf0 . x0) * (r * ((x `| Z) . x0)) by A45
.= (vf0 . x0) * ((r (#) (x `| Z)) . x0) by A47, VALUED_1:def 5
.= (vf0 (#) (r (#) (x `| Z))) . x0 by A46, VALUED_1:def 4
.= (r (#) (vf0 (#) (x `| Z))) . x0 by RFUNCT_1:13 ;
hence (v0 (#) (x `| Z)) . x0 = (r (#) (vf0 (#) (x `| Z))) . x0 ; :: thesis: verum

end;

hence v0 (#) (x `| Z) = r (#) (vf0 (#) (x `| Z)) by A14, A36, A37, FUNCT_1:2; :: thesis: verum

end;

A48: u0 (#) (y `| Z) = r (#) (uf0 (#) (y `| Z))

proof

A49: dom (r (#) (uf0 (#) (y `| Z))) = dom (uf0 (#) (r (#) (y `| Z))) by RFUNCT_1:13
.= (dom uf0) /\ (dom (r (#) (y `| Z))) by VALUED_1:def 4
.= (dom uf0) /\ (dom (y `| Z)) by VALUED_1:def 5 ;
A50: dom (u0 (#) (y `| Z)) = (dom u0) /\ (dom (y `| Z)) by VALUED_1:def 4;
A51: dom (u0 (#) (y `| Z)) = dom (r (#) (uf0 (#) (y `| Z))) by A6, A49, VALUED_1:def 4;
for x0 being object st x0 in dom (u0 (#) (y `| Z)) holds
(u0 (#) (y `| Z)) . x0 = (r (#) (uf0 (#) (y `| Z))) . x0

proof

let x0 be object ; :: thesis: ( x0 in dom (u0 (#) (y `| Z)) implies (u0 (#) (y `| Z)) . x0 = (r (#) (uf0 (#) (y `| Z))) . x0 )
assume A52: x0 in dom (u0 (#) (y `| Z)) ; :: thesis: (u0 (#) (y `| Z)) . x0 = (r (#) (uf0 (#) (y `| Z))) . x0
A53: x0 in (dom u0) /\ (dom (y `| Z)) by A52, VALUED_1:def 4;
then A54: ( x0 in dom u0 & x0 in dom (y `| Z) ) by XBOOLE_0:def 4;
then A55: ( x0 in dom <:x,y:> & <:x,y:> . x0 in dom ((Re (r (#) f)) * R2-to-C) ) by A5, FUNCT_1:11;
set R2 = <:x,y:> . x0;
set c0 = R2-to-C . (<:x,y:> . x0);
A56: u0 . x0 = ((Re (r (#) f)) * R2-to-C) . (<:x,y:> . x0) by A5, A54, FUNCT_1:12
.= (Re (r (#) f)) . (R2-to-C . (<:x,y:> . x0)) by A55, FUNCT_1:12
.= (r (#) (Re f)) . (R2-to-C . (<:x,y:> . x0)) by MESFUN6C:2 ;
x0 in dom uf0 by A6, A53, XBOOLE_0:def 4;
then A57: ( x0 in dom <:x,y:> & <:x,y:> . x0 in dom ((Re f) * R2-to-C) ) by A3, FUNCT_1:11;
A58: uf0 . x0 = ((Re f) * R2-to-C) . (<:x,y:> . x0) by A3, A6, A54, FUNCT_1:12
.= (Re f) . (R2-to-C . (<:x,y:> . x0)) by A57, FUNCT_1:12 ;
A59: x0 in dom (uf0 (#) (r (#) (y `| Z))) by A51, A52, RFUNCT_1:13;
then x0 in (dom uf0) /\ (dom (r (#) (y `| Z))) by VALUED_1:def 4;
then A60: x0 in dom (r (#) (y `| Z)) by XBOOLE_0:def 4;
(u0 (#) (y `| Z)) . x0 = (u0 . x0) * ((y `| Z) . x0) by A52, VALUED_1:def 4
.= (r * ((Re f) . (R2-to-C . (<:x,y:> . x0)))) * ((y `| Z) . x0) by A56, VALUED_1:6
.= (uf0 . x0) * (r * ((y `| Z) . x0)) by A58
.= (uf0 . x0) * ((r (#) (y `| Z)) . x0) by A60, VALUED_1:def 5
.= (uf0 (#) (r (#) (y `| Z))) . x0 by A59, VALUED_1:def 4
.= (r (#) (uf0 (#) (y `| Z))) . x0 by RFUNCT_1:13 ;
hence (u0 (#) (y `| Z)) . x0 = (r (#) (uf0 (#) (y `| Z))) . x0 ; :: thesis: verum

end;

hence u0 (#) (y `| Z) = r (#) (uf0 (#) (y `| Z)) by A6, A49, A50, FUNCT_1:2; :: thesis: verum

end;

A61: v0 (#) (y `| Z) = r (#) (vf0 (#) (y `| Z))

proof

A62: dom (r (#) (vf0 (#) (y `| Z))) = dom (vf0 (#) (r (#) (y `| Z))) by RFUNCT_1:13
.= (dom vf0) /\ (dom (r (#) (y `| Z))) by VALUED_1:def 4
.= (dom vf0) /\ (dom (y `| Z)) by VALUED_1:def 5 ;
A63: dom (v0 (#) (y `| Z)) = (dom v0) /\ (dom (y `| Z)) by VALUED_1:def 4;
A64: dom (v0 (#) (y `| Z)) = dom (r (#) (vf0 (#) (y `| Z))) by A14, A62, VALUED_1:def 4;
for x0 being object st x0 in dom (v0 (#) (y `| Z)) holds
(v0 (#) (y `| Z)) . x0 = (r (#) (vf0 (#) (y `| Z))) . x0

proof

let x0 be object ; :: thesis: ( x0 in dom (v0 (#) (y `| Z)) implies (v0 (#) (y `| Z)) . x0 = (r (#) (vf0 (#) (y `| Z))) . x0 )
assume A65: x0 in dom (v0 (#) (y `| Z)) ; :: thesis: (v0 (#) (y `| Z)) . x0 = (r (#) (vf0 (#) (y `| Z))) . x0
A66: x0 in (dom v0) /\ (dom (y `| Z)) by A65, VALUED_1:def 4;
then A67: ( x0 in dom v0 & x0 in dom (y `| Z) ) by XBOOLE_0:def 4;
then A68: ( x0 in dom <:x,y:> & <:x,y:> . x0 in dom ((Im (r (#) f)) * R2-to-C) ) by A5, FUNCT_1:11;
set R2 = <:x,y:> . x0;
set c0 = R2-to-C . (<:x,y:> . x0);
A69: v0 . x0 = ((Im (r (#) f)) * R2-to-C) . (<:x,y:> . x0) by A5, A67, FUNCT_1:12
.= (Im (r (#) f)) . (R2-to-C . (<:x,y:> . x0)) by A68, FUNCT_1:12
.= (r (#) (Im f)) . (R2-to-C . (<:x,y:> . x0)) by MESFUN6C:2 ;
x0 in dom vf0 by A14, A66, XBOOLE_0:def 4;
then A70: ( x0 in dom <:x,y:> & <:x,y:> . x0 in dom ((Im f) * R2-to-C) ) by A3, FUNCT_1:11;
A71: vf0 . x0 = ((Im f) * R2-to-C) . (<:x,y:> . x0) by A3, A14, A67, FUNCT_1:12
.= (Im f) . (R2-to-C . (<:x,y:> . x0)) by A70, FUNCT_1:12 ;
A72: x0 in dom (vf0 (#) (r (#) (y `| Z))) by A64, A65, RFUNCT_1:13;
then x0 in (dom vf0) /\ (dom (r (#) (y `| Z))) by VALUED_1:def 4;
then A73: x0 in dom (r (#) (y `| Z)) by XBOOLE_0:def 4;
(v0 (#) (y `| Z)) . x0 = (v0 . x0) * ((y `| Z) . x0) by A65, VALUED_1:def 4
.= (r * ((Im f) . (R2-to-C . (<:x,y:> . x0)))) * ((y `| Z) . x0) by A69, VALUED_1:6
.= (vf0 . x0) * (r * ((y `| Z) . x0)) by A71
.= (vf0 . x0) * ((r (#) (y `| Z)) . x0) by A73, VALUED_1:def 5
.= (vf0 (#) (r (#) (y `| Z))) . x0 by A72, VALUED_1:def 4
.= (r (#) (vf0 (#) (y `| Z))) . x0 by RFUNCT_1:13 ;
hence (v0 (#) (y `| Z)) . x0 = (r (#) (vf0 (#) (y `| Z))) . x0 ; :: thesis: verum

end;

hence v0 (#) (y `| Z) = r (#) (vf0 (#) (y `| Z)) by A14, A62, A63, FUNCT_1:2; :: thesis: verum

end;

A74: [.a,b.] c= dom uf0

proof

let x0 be object ; :: according to TARSKI:def 3 :: thesis: ( not x0 in [.a,b.] or x0 in dom uf0 )
assume A75: x0 in [.a,b.] ; :: thesis: x0 in dom uf0
A76: C . x0 in rng C by A2, A75, FUNCT_1:3;
A77: ( x0 in dom x & x0 in dom y ) by A2, A75;
A78: x0 in (dom x) /\ (dom y) by A2, A75, XBOOLE_0:def 4;
then A79: x0 in dom <:x,y:> by FUNCT_3:def 7;
set R2 = <:x,y:> . x0;
reconsider xx0 = x . x0, yx0 = y . x0 as Element of REAL by XREAL_0:def 1;
<:x,y:> . x0 = [xx0,yx0] by A78, FUNCT_3:48;
then <:x,y:> . x0 in [:REAL,REAL:] by ZFMISC_1:def 2;
then A80: <:x,y:> . x0 in dom R2-to-C by FUNCT_2:def 1;
x0 in dom (<i> (#) y) by A77, VALUED_1:def 5;
then x0 in (dom x) /\ (dom (<i> (#) y)) by A2, A75, XBOOLE_0:def 4;
then A81: x0 in dom (x + (<i> (#) y)) by VALUED_1:def 1;
A82: [xx0,yx0] in [:REAL,REAL:] by ZFMISC_1:def 2;
A83: ( x . x0 = [(x . x0),(y . x0)] `1 & y . x0 = [(x . x0),(y . x0)] `2 ) ;
C . x0 = (x + (<i> (#) y)) . x0 by A75, A2, FUNCT_1:49
.= (x . x0) + ((<i> (#) y) . x0) by A81, VALUED_1:def 1
.= (x . x0) + (<i> * (y . x0)) by VALUED_1:6
.= R2-to-C . [xx0,yx0] by A82, A83, Def1
.= R2-to-C . (<:x,y:> . x0) by A78, FUNCT_3:48 ;
then R2-to-C . (<:x,y:> . x0) in dom f by A1, A76;
then R2-to-C . (<:x,y:> . x0) in dom (Re f) by COMSEQ_3:def 3;
then <:x,y:> . x0 in dom ((Re f) * R2-to-C) by A80, FUNCT_1:11;
hence x0 in dom uf0 by A3, A79, FUNCT_1:11; :: thesis: verum

end;

A84: [.a,b.] c= dom vf0

proof

let x0 be object ; :: according to TARSKI:def 3 :: thesis: ( not x0 in [.a,b.] or x0 in dom vf0 )
assume A85: x0 in [.a,b.] ; :: thesis: x0 in dom vf0
A86: C . x0 in rng C by A2, A85, FUNCT_1:3;
A87: ( x0 in dom x & x0 in dom y ) by A2, A85;
A88: x0 in (dom x) /\ (dom y) by A2, A85, XBOOLE_0:def 4;
then A89: x0 in dom <:x,y:> by FUNCT_3:def 7;
set R2 = <:x,y:> . x0;
reconsider xx0 = x . x0, yx0 = y . x0 as Element of REAL by XREAL_0:def 1;
<:x,y:> . x0 = [xx0,yx0] by A88, FUNCT_3:48;
then <:x,y:> . x0 in [:REAL,REAL:] by ZFMISC_1:def 2;
then A90: <:x,y:> . x0 in dom R2-to-C by FUNCT_2:def 1;
x0 in dom (<i> (#) y) by A87, VALUED_1:def 5;
then x0 in (dom x) /\ (dom (<i> (#) y)) by A2, A85, XBOOLE_0:def 4;
then A91: x0 in dom (x + (<i> (#) y)) by VALUED_1:def 1;
A92: [xx0,yx0] in [:REAL,REAL:] by ZFMISC_1:def 2;
A93: ( x . x0 = [(x . x0),(y . x0)] `1 & y . x0 = [(x . x0),(y . x0)] `2 ) ;
C . x0 = (x + (<i> (#) y)) . x0 by A85, A2, FUNCT_1:49
.= (x . x0) + ((<i> (#) y) . x0) by A91, VALUED_1:def 1
.= (x . x0) + (<i> * (y . x0)) by VALUED_1:6
.= R2-to-C . [xx0,yx0] by A92, A93, Def1
.= R2-to-C . (<:x,y:> . x0) by A88, FUNCT_3:48 ;
then R2-to-C . (<:x,y:> . x0) in dom f by A1, A86;
then R2-to-C . (<:x,y:> . x0) in dom (Im f) by COMSEQ_3:def 4;
then <:x,y:> . x0 in dom ((Im f) * R2-to-C) by A90, FUNCT_1:11;
hence x0 in dom vf0 by A3, A89, FUNCT_1:11; :: thesis: verum

end;

A94: ['a,b'] c= dom ((uf0 (#) (x `| Z)) - (vf0 (#) (y `| Z)))

proof

A95: ['a,b'] = [.a,b.] by A2, INTEGRA5:def 3;
A96: dom ((uf0 (#) (x `| Z)) - (vf0 (#) (y `| Z))) = (dom (uf0 (#) (x `| Z))) /\ (dom (vf0 (#) (y `| Z))) by VALUED_1:12
.= ((dom uf0) /\ (dom (x `| Z))) /\ (dom (vf0 (#) (y `| Z))) by VALUED_1:def 4
.= ((dom uf0) /\ (dom (x `| Z))) /\ ((dom vf0) /\ (dom (y `| Z))) by VALUED_1:def 4
.= (dom uf0) /\ ((dom (x `| Z)) /\ ((dom vf0) /\ (dom (y `| Z)))) by XBOOLE_1:16
.= (dom uf0) /\ (Z /\ ((dom (y `| Z)) /\ (dom vf0))) by A2, FDIFF_1:def 7
.= (dom uf0) /\ (Z /\ (Z /\ (dom vf0))) by A2, FDIFF_1:def 7
.= (dom uf0) /\ ((Z /\ Z) /\ (dom vf0)) by XBOOLE_1:16
.= ((dom uf0) /\ (dom vf0)) /\ Z by XBOOLE_1:16 ;
[.a,b.] c= (dom uf0) /\ (dom vf0) by A74, A84, XBOOLE_1:19;
hence ['a,b'] c= dom ((uf0 (#) (x `| Z)) - (vf0 (#) (y `| Z))) by A2, A95, A96, XBOOLE_1:19; :: thesis: verum

end;

A97: ['a,b'] c= dom ((vf0 (#) (x `| Z)) + (uf0 (#) (y `| Z)))

proof

A98: ['a,b'] = [.a,b.] by A2, INTEGRA5:def 3;
A99: dom ((vf0 (#) (x `| Z)) + (uf0 (#) (y `| Z))) = (dom (vf0 (#) (x `| Z))) /\ (dom (uf0 (#) (y `| Z))) by VALUED_1:def 1
.= ((dom vf0) /\ (dom (x `| Z))) /\ (dom (uf0 (#) (y `| Z))) by VALUED_1:def 4
.= ((dom vf0) /\ (dom (x `| Z))) /\ ((dom uf0) /\ (dom (y `| Z))) by VALUED_1:def 4
.= (dom vf0) /\ ((dom (x `| Z)) /\ ((dom uf0) /\ (dom (y `| Z)))) by XBOOLE_1:16
.= (dom vf0) /\ (Z /\ ((dom (y `| Z)) /\ (dom uf0))) by A2, FDIFF_1:def 7
.= (dom vf0) /\ (Z /\ (Z /\ (dom uf0))) by A2, FDIFF_1:def 7
.= (dom vf0) /\ ((Z /\ Z) /\ (dom uf0)) by XBOOLE_1:16
.= ((dom vf0) /\ (dom uf0)) /\ Z by XBOOLE_1:16 ;
[.a,b.] c= (dom vf0) /\ (dom uf0) by A74, A84, XBOOLE_1:19;
hence ['a,b'] c= dom ((vf0 (#) (x `| Z)) + (uf0 (#) (y `| Z))) by A2, A98, A99, XBOOLE_1:19; :: thesis: verum

end;

reconsider a = a, b = b as Real ;
A100: (uf0 (#) (x `| Z)) - (vf0 (#) (y `| Z)) is_integrable_on ['a,b'] by A1, A2;
A101: (vf0 (#) (x `| Z)) + (uf0 (#) (y `| Z)) is_integrable_on ['a,b'] by A1, A2;
A102: ((uf0 (#) (x `| Z)) - (vf0 (#) (y `| Z))) | ['a,b'] is bounded by A1, A2;
A103: ((vf0 (#) (x `| Z)) + (uf0 (#) (y `| Z))) | ['a,b'] is bounded by A1, A2;
integral ((r (#) f),C) = (integral (((r (#) (uf0 (#) (x `| Z))) - (r (#) (vf0 (#) (y `| Z)))),a,b)) + ((integral (((r (#) (vf0 (#) (x `| Z))) + (r (#) (uf0 (#) (y `| Z)))),a,b)) * <i>) by A35, A61, A48, A22, A5, A1, A2, A4, Def4
.= (integral ((r (#) ((uf0 (#) (x `| Z)) - (vf0 (#) (y `| Z)))),a,b)) + ((integral (((r (#) (vf0 (#) (x `| Z))) + (r (#) (uf0 (#) (y `| Z)))),a,b)) * <i>) by RFUNCT_1:18
.= (integral ((r (#) ((uf0 (#) (x `| Z)) - (vf0 (#) (y `| Z)))),a,b)) + ((integral ((r (#) ((vf0 (#) (x `| Z)) + (uf0 (#) (y `| Z)))),a,b)) * <i>) by RFUNCT_1:16
.= (r * (integral (((uf0 (#) (x `| Z)) - (vf0 (#) (y `| Z))),a,b))) + ((integral ((r (#) ((vf0 (#) (x `| Z)) + (uf0 (#) (y `| Z)))),a,b)) * <i>) by A2, A94, A100, A102, INTEGRA6:10
.= (r * (integral (((uf0 (#) (x `| Z)) - (vf0 (#) (y `| Z))),a,b))) + ((r * (integral (((vf0 (#) (x `| Z)) + (uf0 (#) (y `| Z))),a,b))) * <i>) by A2, A97, A101, A103, INTEGRA6:10
.= r * ((integral (((uf0 (#) (x `| Z)) - (vf0 (#) (y `| Z))),a,b)) + ((integral (((vf0 (#) (x `| Z)) + (uf0 (#) (y `| Z))),a,b)) * <i>))
.= r * (integral (f,C)) by A1, A2, A3, Def4 ;
hence integral ((r (#) f),C) = r * (integral (f,C)) ; :: thesis: verum