let s1, s2 be Complex; :: thesis: ( ex a, b being Real ex x, y being PartFunc of REAL,REAL ex Z being Subset of REAL st
( 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.] & s1 = integral (f,x,y,a,b,Z) ) & ex a, b being Real ex x, y being PartFunc of REAL,REAL ex Z being Subset of REAL st
( 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.] & s2 = integral (f,x,y,a,b,Z) ) implies s1 = s2 )
assume A3: ex a, b being Real ex x, y being PartFunc of REAL,REAL ex Z being Subset of REAL st
( 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.] & s1 = integral (f,x,y,a,b,Z) ) ; :: thesis: ( for a, b being Real
for x, y being PartFunc of REAL,REAL
for Z being Subset of REAL holds
( not a <= b or not [.a,b.] = dom C or not [.a,b.] c= dom x or not [.a,b.] c= dom y or not Z is open or not [.a,b.] c= Z or not x is_differentiable_on Z or not y is_differentiable_on Z or not x `| Z is continuous or not y `| Z is continuous or not C = (x + (<i> (#) y)) | [.a,b.] or not s2 = integral (f,x,y,a,b,Z) ) or s1 = s2 )
assume A4: ex a, b being Real ex x, y being PartFunc of REAL,REAL ex Z being Subset of REAL st
( 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.] & s2 = integral (f,x,y,a,b,Z) ) ; :: thesis: s1 = s2
consider a1, b1 being Real, x1, y1 being PartFunc of REAL,REAL, Z1 being Subset of REAL such that
A5: ( a1 <= b1 & [.a1,b1.] = dom C & [.a1,b1.] c= dom x1 & [.a1,b1.] c= dom y1 & Z1 is open & [.a1,b1.] c= Z1 & x1 is_differentiable_on Z1 & y1 is_differentiable_on Z1 & x1 `| Z1 is continuous & y1 `| Z1 is continuous & C = (x1 + (<i> (#) y1)) | [.a1,b1.] & s1 = integral (f,x1,y1,a1,b1,Z1) ) by A3;
consider a2, b2 being Real, x2, y2 being PartFunc of REAL,REAL, Z2 being Subset of REAL such that
A6: ( a2 <= b2 & [.a2,b2.] = dom C & [.a2,b2.] c= dom x2 & [.a2,b2.] c= dom y2 & Z2 is open & [.a2,b2.] c= Z2 & x2 is_differentiable_on Z2 & y2 is_differentiable_on Z2 & x2 `| Z2 is continuous & y2 `| Z2 is continuous & C = (x2 + (<i> (#) y2)) | [.a2,b2.] & s2 = integral (f,x2,y2,a2,b2,Z2) ) by A4;
dom C is non empty closed_interval Subset of REAL by A5, MEASURE5:14;
then A7: ( a1 = a2 & b1 = b2 ) by A6, A5, INTEGRA1:5;
reconsider Z3 = Z1 /\ Z2 as Subset of REAL ;
reconsider ZZ1 = Z1, ZZ2 = Z2 as Subset of R^1 by TOPMETR:17;
( ZZ1 is open & ZZ2 is open ) by A5, A6, BORSUK_5:39;
then ZZ1 /\ ZZ2 is open by TOPS_1:11;
then A8: Z3 is open by BORSUK_5:39;
A9: x1 | [.a1,b1.] = x2 | [.a2,b2.]

proof

for x0 being set st x0 in [.a1,b1.] holds
x1 . x0 = x2 . x0

proof

let x0 be set ; :: thesis: ( x0 in [.a1,b1.] implies x1 . x0 = x2 . x0 )
assume A10: x0 in [.a1,b1.] ; :: thesis: x1 . x0 = x2 . x0
A11: dom (<i> (#) y1) = dom y1 by VALUED_1:def 5;
dom (x1 + (<i> (#) y1)) = (dom x1) /\ (dom (<i> (#) y1)) by VALUED_1:def 1;
then A12: [.a1,b1.] c= dom (x1 + (<i> (#) y1)) by A5, A11, XBOOLE_1:19;
A13: ((x1 + (<i> (#) y1)) | [.a1,b1.]) . x0 = (x1 + (<i> (#) y1)) . x0 by A10, FUNCT_1:49
.= (x1 . x0) + ((<i> (#) y1) . x0) by A10, A12, VALUED_1:def 1
.= (x1 . x0) + (<i> * (y1 . x0)) by VALUED_1:6 ;
A14: dom (<i> (#) y2) = dom y2 by VALUED_1:def 5;
dom (x2 + (<i> (#) y2)) = (dom x2) /\ (dom (<i> (#) y2)) by VALUED_1:def 1;
then A15: [.a2,b2.] c= dom (x2 + (<i> (#) y2)) by A6, A14, XBOOLE_1:19;
((x2 + (<i> (#) y2)) | [.a2,b2.]) . x0 = (x2 + (<i> (#) y2)) . x0 by A6, A5, A10, FUNCT_1:49
.= (x2 . x0) + ((<i> (#) y2) . x0) by A6, A5, A10, A15, VALUED_1:def 1
.= (x2 . x0) + (<i> * (y2 . x0)) by VALUED_1:6 ;
hence x1 . x0 = x2 . x0 by A6, A5, A13, COMPLEX1:77; :: thesis: verum

end;

hence x1 | [.a1,b1.] = x2 | [.a2,b2.] by A5, A6, FUNCT_1:95; :: thesis: verum

end;

A16: y1 | [.a1,b1.] = y2 | [.a2,b2.]

proof

for x0 being set st x0 in [.a1,b1.] holds
y1 . x0 = y2 . x0

proof

let x0 be set ; :: thesis: ( x0 in [.a1,b1.] implies y1 . x0 = y2 . x0 )
assume A17: x0 in [.a1,b1.] ; :: thesis: y1 . x0 = y2 . x0
A18: dom (<i> (#) y1) = dom y1 by VALUED_1:def 5;
dom (x1 + (<i> (#) y1)) = (dom x1) /\ (dom (<i> (#) y1)) by VALUED_1:def 1;
then A19: [.a1,b1.] c= dom (x1 + (<i> (#) y1)) by A5, A18, XBOOLE_1:19;
A20: ((x1 + (<i> (#) y1)) | [.a1,b1.]) . x0 = (x1 + (<i> (#) y1)) . x0 by A17, FUNCT_1:49
.= (x1 . x0) + ((<i> (#) y1) . x0) by A17, A19, VALUED_1:def 1
.= (x1 . x0) + (<i> * (y1 . x0)) by VALUED_1:6 ;
A21: dom (<i> (#) y2) = dom y2 by VALUED_1:def 5;
dom (x2 + (<i> (#) y2)) = (dom x2) /\ (dom (<i> (#) y2)) by VALUED_1:def 1;
then A22: [.a2,b2.] c= dom (x2 + (<i> (#) y2)) by A6, A21, XBOOLE_1:19;
((x2 + (<i> (#) y2)) | [.a2,b2.]) . x0 = (x2 + (<i> (#) y2)) . x0 by A5, A6, A17, FUNCT_1:49
.= (x2 . x0) + ((<i> (#) y2) . x0) by A5, A6, A17, A22, VALUED_1:def 1
.= (x2 . x0) + (<i> * (y2 . x0)) by VALUED_1:6 ;
hence y1 . x0 = y2 . x0 by A6, A5, A20, COMPLEX1:77; :: thesis: verum

end;

hence y1 | [.a1,b1.] = y2 | [.a2,b2.] by A5, A6, FUNCT_1:95; :: thesis: verum

end;

A23: [.a1,b1.] c= Z3 by A5, A6, XBOOLE_1:19;
A24: ( x1 is_differentiable_on Z3 & y1 is_differentiable_on Z3 ) by A5, A8, FDIFF_1:26, XBOOLE_1:17;
A25: ( x2 is_differentiable_on Z3 & y2 is_differentiable_on Z3 ) by A6, A8, FDIFF_1:26, XBOOLE_1:17;
thus s1 = integral (f,x1,y1,a1,b1,Z3) by A1, A5, A8, A23, Lm1, XBOOLE_1:17
.= integral (f,x2,y2,a2,b2,Z3) by A1, A5, A6, A7, A8, A9, A16, A24, A25, Lm2, XBOOLE_1:19
.= s2 by A1, A6, A5, A8, A23, Lm1, XBOOLE_1:17 ; :: thesis: verum