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;
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 set st x0 in dom u0 holds
x0 in dom uf0

proof

let x0 be set ; :: 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:21;
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:21;
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:21;
hence x0 in dom uf0 by A3, A9, FUNCT_1:21; :: thesis: verum

end;

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

proof

let x0 be set ; :: 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:21;
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:21;
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:21;
hence x0 in dom u0 by A5, A12, FUNCT_1:21; :: 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 set st x0 in dom v0 holds
x0 in dom vf0

proof

let x0 be set ; :: 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:21;
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:21;
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:21;
hence x0 in dom vf0 by A3, A17, FUNCT_1:21; :: thesis: verum

end;

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

proof

let x0 be set ; :: 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:21;
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:21;
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:21;
hence x0 in dom v0 by A5, A20, FUNCT_1:21; :: 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:25
.= (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 set st x0 in dom (u0 (#) (x `| Z)) holds
(u0 (#) (x `| Z)) . x0 = (r (#) (uf0 (#) (x `| Z))) . x0

proof

let x0 be set ; :: 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:21;
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:22
.= (Re (r (#) f)) . (R2-to-C . (<:x,y:> . x0)) by A29, FUNCT_1:22
.= (r (#) (Re f)) . (R2-to-C . (<:x,y:> . x0)) by MESFUN6C:2 ;
x0 in dom uf0 by A6, A27, XBOOLE_0:def 4;
then A32: ( x0 in dom <:x,y:> & <:x,y:> . x0 in dom ((Re f) * R2-to-C ) ) by A3, FUNCT_1:21;
A33: uf0 . x0 = ((Re f) * R2-to-C ) . (<:x,y:> . x0) by A3, A6, A28, FUNCT_1:22
.= (Re f) . (R2-to-C . (<:x,y:> . x0)) by A32, FUNCT_1:22 ;
A34: x0 in dom (uf0 (#) (r (#) (x `| Z))) by A26, A25, RFUNCT_1:25;
then x0 in (dom uf0) /\ (dom (r (#) (x `| Z))) by VALUED_1:def 4;
then A35: 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 A33
.= (uf0 . x0) * ((r (#) (x `| Z)) . x0) by A35, VALUED_1:def 5
.= (uf0 (#) (r (#) (x `| Z))) . x0 by A34, VALUED_1:def 4
.= (r (#) (uf0 (#) (x `| Z))) . x0 by RFUNCT_1:25 ;
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:9; :: thesis: verum

end;

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

proof

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

proof

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

end;

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

end;

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

proof

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

proof

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

end;

hence u0 (#) (y `| Z) = r (#) (uf0 (#) (y `| Z)) by A6, A51, A52, FUNCT_1:9; :: thesis: verum

end;

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

proof

A65: dom (r (#) (vf0 (#) (y `| Z))) = dom (vf0 (#) (r (#) (y `| Z))) by RFUNCT_1:25
.= (dom vf0) /\ (dom (r (#) (y `| Z))) by VALUED_1:def 4
.= (dom vf0) /\ (dom (y `| Z)) by VALUED_1:def 5 ;
A66: dom (v0 (#) (y `| Z)) = (dom v0) /\ (dom (y `| Z)) by VALUED_1:def 4;
A67: dom (v0 (#) (y `| Z)) = dom (r (#) (vf0 (#) (y `| Z))) by A14, A65, VALUED_1:def 4;
for x0 being set st x0 in dom (v0 (#) (y `| Z)) holds
(v0 (#) (y `| Z)) . x0 = (r (#) (vf0 (#) (y `| Z))) . x0

proof

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

end;

hence v0 (#) (y `| Z) = r (#) (vf0 (#) (y `| Z)) by A14, A65, A66, FUNCT_1:9; :: thesis: verum

end;

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

proof

for x0 being set st x0 in [.a,b.] holds
x0 in dom uf0

proof

let x0 be set ; :: thesis: ( x0 in [.a,b.] implies x0 in dom uf0 )
assume A79: x0 in [.a,b.] ; :: thesis: x0 in dom uf0
A80: C . x0 in rng C by A2, A79, FUNCT_1:12;
A81: ( x0 in dom x & x0 in dom y ) by A2, A79;
A82: x0 in (dom x) /\ (dom y) by A2, A79, XBOOLE_0:def 4;
then A83: x0 in dom <:x,y:> by FUNCT_3:def 8;
set R2 = <:x,y:> . x0;
<:x,y:> . x0 = [(x . x0),(y . x0)] by A82, FUNCT_3:68;
then <:x,y:> . x0 in [:REAL ,REAL :] by ZFMISC_1:def 2;
then A84: <:x,y:> . x0 in dom R2-to-C by FUNCT_2:def 1;
x0 in dom (<i> (#) y) by A81, VALUED_1:def 5;
then x0 in (dom x) /\ (dom (<i> (#) y)) by A2, A79, XBOOLE_0:def 4;
then A85: x0 in dom (x + (<i> (#) y)) by VALUED_1:def 1;
A86: [(x . x0),(y . x0)] in [:REAL ,REAL :] by ZFMISC_1:def 2;
A87: ( x . x0 = [(x . x0),(y . x0)] `1 & y . x0 = [(x . x0),(y . x0)] `2 ) by MCART_1:7;
C . x0 = (x + (<i> (#) y)) . x0 by A79, FUNCT_1:72, A2
.= (x . x0) + ((<i> (#) y) . x0) by A85, VALUED_1:def 1
.= (x . x0) + (<i> * (y . x0)) by VALUED_1:6
.= R2-to-C . [(x . x0),(y . x0)] by A86, A87, Def1
.= R2-to-C . (<:x,y:> . x0) by A82, FUNCT_3:68 ;
then R2-to-C . (<:x,y:> . x0) in dom f by A1, A80;
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 A84, FUNCT_1:21;
hence x0 in dom uf0 by A3, A83, FUNCT_1:21; :: thesis: verum

end;

hence [.a,b.] c= dom uf0 by TARSKI:def 3; :: thesis: verum

end;

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

proof

for x0 being set st x0 in [.a,b.] holds
x0 in dom vf0

proof

let x0 be set ; :: thesis: ( x0 in [.a,b.] implies x0 in dom vf0 )
assume A89: x0 in [.a,b.] ; :: thesis: x0 in dom vf0
A90: C . x0 in rng C by A2, A89, FUNCT_1:12;
A91: ( x0 in dom x & x0 in dom y ) by A2, A89;
A92: x0 in (dom x) /\ (dom y) by A2, A89, XBOOLE_0:def 4;
then A93: x0 in dom <:x,y:> by FUNCT_3:def 8;
set R2 = <:x,y:> . x0;
<:x,y:> . x0 = [(x . x0),(y . x0)] by A92, FUNCT_3:68;
then <:x,y:> . x0 in [:REAL ,REAL :] by ZFMISC_1:def 2;
then A94: <:x,y:> . x0 in dom R2-to-C by FUNCT_2:def 1;
x0 in dom (<i> (#) y) by A91, VALUED_1:def 5;
then x0 in (dom x) /\ (dom (<i> (#) y)) by A2, A89, XBOOLE_0:def 4;
then A95: x0 in dom (x + (<i> (#) y)) by VALUED_1:def 1;
A96: [(x . x0),(y . x0)] in [:REAL ,REAL :] by ZFMISC_1:def 2;
A97: ( x . x0 = [(x . x0),(y . x0)] `1 & y . x0 = [(x . x0),(y . x0)] `2 ) by MCART_1:7;
C . x0 = (x + (<i> (#) y)) . x0 by A89, FUNCT_1:72, A2
.= (x . x0) + ((<i> (#) y) . x0) by A95, VALUED_1:def 1
.= (x . x0) + (<i> * (y . x0)) by VALUED_1:6
.= R2-to-C . [(x . x0),(y . x0)] by A96, A97, Def1
.= R2-to-C . (<:x,y:> . x0) by A92, FUNCT_3:68 ;
then R2-to-C . (<:x,y:> . x0) in dom f by A1, A90;
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 A94, FUNCT_1:21;
hence x0 in dom vf0 by A3, A93, FUNCT_1:21; :: thesis: verum

end;

hence [.a,b.] c= dom vf0 by TARSKI:def 3; :: thesis: verum

end;

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

proof

A99: ['a,b'] = [.a,b.] by A2, INTEGRA5:def 4;
A100: 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 8
.= (dom uf0) /\ (Z /\ (Z /\ (dom vf0))) by A2, FDIFF_1:def 8
.= (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 A78, A88, XBOOLE_1:19;
hence ['a,b'] c= dom ((uf0 (#) (x `| Z)) - (vf0 (#) (y `| Z))) by A2, A99, A100, XBOOLE_1:19; :: thesis: verum

end;

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

proof

A102: ['a,b'] = [.a,b.] by A2, INTEGRA5:def 4;
A103: 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 8
.= (dom vf0) /\ (Z /\ (Z /\ (dom uf0))) by A2, FDIFF_1:def 8
.= (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 A78, A88, XBOOLE_1:19;
hence ['a,b'] c= dom ((vf0 (#) (x `| Z)) + (uf0 (#) (y `| Z))) by A2, A102, A103, XBOOLE_1:19; :: thesis: verum

end;

A104: (uf0 (#) (x `| Z)) - (vf0 (#) (y `| Z)) is_integrable_on ['a,b'] by A1, A2, Def5;
A105: (vf0 (#) (x `| Z)) + (uf0 (#) (y `| Z)) is_integrable_on ['a,b'] by A1, A2, Def5;
A106: ((uf0 (#) (x `| Z)) - (vf0 (#) (y `| Z))) | ['a,b'] is bounded by A1, A2, Def6;
A107: ((vf0 (#) (x `| Z)) + (uf0 (#) (y `| Z))) | ['a,b'] is bounded by A1, A2, Def6;
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 A36, A64, A50, 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:30
.= (integral (r (#) ((uf0 (#) (x `| Z)) - (vf0 (#) (y `| Z)))),a,b) + ((integral (r (#) ((vf0 (#) (x `| Z)) + (uf0 (#) (y `| Z)))),a,b) * <i> ) by RFUNCT_1:28
.= (r * (integral ((uf0 (#) (x `| Z)) - (vf0 (#) (y `| Z))),a,b)) + ((integral (r (#) ((vf0 (#) (x `| Z)) + (uf0 (#) (y `| Z)))),a,b) * <i> ) by A2, A98, A104, A106, 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, A101, A105, A107, 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