let T be non empty TopSpace; for f being FinSequence of Curves T st len f > 0 & ( for i being Nat st 1 <= i & i < len f holds
( (f /. i) . (sup (dom (f /. i))) = (f /. (i + 1)) . (inf (dom (f /. (i + 1)))) & sup (dom (f /. i)) = inf (dom (f /. (i + 1))) ) ) & ( for i being Nat st 1 <= i & i <= len f holds
f /. i is with_endpoints ) holds
ex c being with_endpoints Curve of T st
( Sum f = c & dom c = [.(inf (dom (f /. 1))),(sup (dom (f /. (len f)))).] & the_first_point_of c = (f /. 1) . (inf (dom (f /. 1))) & the_last_point_of c = (f /. (len f)) . (sup (dom (f /. (len f)))) )
defpred S1[ Nat] means for f being FinSequence of Curves T st len f = $1 & len f > 0 & ( for i being Nat st 1 <= i & i < len f holds
( (f /. i) . (sup (dom (f /. i))) = (f /. (i + 1)) . (inf (dom (f /. (i + 1)))) & sup (dom (f /. i)) = inf (dom (f /. (i + 1))) ) ) & ( for i being Nat st 1 <= i & i <= len f holds
f /. i is with_endpoints ) holds
ex c being with_endpoints Curve of T st
( Sum f = c & dom c = [.(inf (dom (f /. 1))),(sup (dom (f /. (len f)))).] & the_first_point_of c = (f /. 1) . (inf (dom (f /. 1))) & the_last_point_of c = (f /. (len f)) . (sup (dom (f /. (len f)))) );
A1:
S1[ 0 ]
;
A2:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A3:
S1[
k]
;
S1[k + 1]
let f be
FinSequence of
Curves T;
( len f = k + 1 & len f > 0 & ( for i being Nat st 1 <= i & i < len f holds
( (f /. i) . (sup (dom (f /. i))) = (f /. (i + 1)) . (inf (dom (f /. (i + 1)))) & sup (dom (f /. i)) = inf (dom (f /. (i + 1))) ) ) & ( for i being Nat st 1 <= i & i <= len f holds
f /. i is with_endpoints ) implies ex c being with_endpoints Curve of T st
( Sum f = c & dom c = [.(inf (dom (f /. 1))),(sup (dom (f /. (len f)))).] & the_first_point_of c = (f /. 1) . (inf (dom (f /. 1))) & the_last_point_of c = (f /. (len f)) . (sup (dom (f /. (len f)))) ) )
assume A4:
(
len f = k + 1 &
len f > 0 )
;
( ex i being Nat st
( 1 <= i & i < len f & not ( (f /. i) . (sup (dom (f /. i))) = (f /. (i + 1)) . (inf (dom (f /. (i + 1)))) & sup (dom (f /. i)) = inf (dom (f /. (i + 1))) ) ) or ex i being Nat st
( 1 <= i & i <= len f & not f /. i is with_endpoints ) or ex c being with_endpoints Curve of T st
( Sum f = c & dom c = [.(inf (dom (f /. 1))),(sup (dom (f /. (len f)))).] & the_first_point_of c = (f /. 1) . (inf (dom (f /. 1))) & the_last_point_of c = (f /. (len f)) . (sup (dom (f /. (len f)))) ) )
consider f1 being
FinSequence of
Curves T,
c2 being
Element of
Curves T such that A5:
f = f1 ^ <*c2*>
by A4, FINSEQ_2:19;
A6:
len f =
(len f1) + (len <*c2*>)
by A5, FINSEQ_1:22
.=
(len f1) + 1
by FINSEQ_1:39
;
assume A7:
for
i being
Nat st 1
<= i &
i < len f holds
(
(f /. i) . (sup (dom (f /. i))) = (f /. (i + 1)) . (inf (dom (f /. (i + 1)))) &
sup (dom (f /. i)) = inf (dom (f /. (i + 1))) )
;
( ex i being Nat st
( 1 <= i & i <= len f & not f /. i is with_endpoints ) or ex c being with_endpoints Curve of T st
( Sum f = c & dom c = [.(inf (dom (f /. 1))),(sup (dom (f /. (len f)))).] & the_first_point_of c = (f /. 1) . (inf (dom (f /. 1))) & the_last_point_of c = (f /. (len f)) . (sup (dom (f /. (len f)))) ) )
assume A8:
for
i being
Nat st 1
<= i &
i <= len f holds
f /. i is
with_endpoints
;
ex c being with_endpoints Curve of T st
( Sum f = c & dom c = [.(inf (dom (f /. 1))),(sup (dom (f /. (len f)))).] & the_first_point_of c = (f /. 1) . (inf (dom (f /. 1))) & the_last_point_of c = (f /. (len f)) . (sup (dom (f /. (len f)))) )
A9:
1
<= len f
by A4, NAT_1:12;
len f in Seg (len f)
by A4, FINSEQ_1:3;
then A10:
len f in dom f
by FINSEQ_1:def 3;
c2 =
f . (len f)
by A5, A6, FINSEQ_1:42
.=
f /. (len f)
by A10, PARTFUN1:def 6
;
then reconsider c2 =
c2 as
with_endpoints Curve of
T by A9, A8;
A11:
for
i being
Nat st 1
<= i &
i < len f1 holds
(
(f1 /. i) . (sup (dom (f1 /. i))) = (f1 /. (i + 1)) . (inf (dom (f1 /. (i + 1)))) &
sup (dom (f1 /. i)) = inf (dom (f1 /. (i + 1))) )
proof
let i be
Nat;
( 1 <= i & i < len f1 implies ( (f1 /. i) . (sup (dom (f1 /. i))) = (f1 /. (i + 1)) . (inf (dom (f1 /. (i + 1)))) & sup (dom (f1 /. i)) = inf (dom (f1 /. (i + 1))) ) )
assume A12:
( 1
<= i &
i < len f1 )
;
( (f1 /. i) . (sup (dom (f1 /. i))) = (f1 /. (i + 1)) . (inf (dom (f1 /. (i + 1)))) & sup (dom (f1 /. i)) = inf (dom (f1 /. (i + 1))) )
A13:
i < len f
by A6, A12, NAT_1:13;
i in Seg (len f1)
by A12, FINSEQ_1:1;
then A14:
i in dom f1
by FINSEQ_1:def 3;
A15:
dom f1 c= dom f
by A5, FINSEQ_1:26;
A16:
f /. i =
f . i
by A15, A14, PARTFUN1:def 6
.=
f1 . i
by A5, A14, FINSEQ_1:def 7
.=
f1 /. i
by A14, PARTFUN1:def 6
;
1
+ 1
<= i + 1
by A12, XREAL_1:6;
then A17:
1
<= i + 1
by XXREAL_0:2;
i + 1
<= len f1
by A12, NAT_1:13;
then
i + 1
in Seg (len f1)
by A17, FINSEQ_1:1;
then A18:
i + 1
in dom f1
by FINSEQ_1:def 3;
A19:
f /. (i + 1) =
f . (i + 1)
by A18, A15, PARTFUN1:def 6
.=
f1 . (i + 1)
by A5, A18, FINSEQ_1:def 7
.=
f1 /. (i + 1)
by A18, PARTFUN1:def 6
;
thus
(
(f1 /. i) . (sup (dom (f1 /. i))) = (f1 /. (i + 1)) . (inf (dom (f1 /. (i + 1)))) &
sup (dom (f1 /. i)) = inf (dom (f1 /. (i + 1))) )
by A16, A19, A13, A12, A7;
verum
end;
A20:
for
i being
Nat st 1
<= i &
i <= len f1 holds
f1 /. i is
with_endpoints
proof
let i be
Nat;
( 1 <= i & i <= len f1 implies f1 /. i is with_endpoints )
assume A21:
( 1
<= i &
i <= len f1 )
;
f1 /. i is with_endpoints
A22:
i <= len f
by A6, A21, NAT_1:13;
i in Seg (len f1)
by A21, FINSEQ_1:1;
then A23:
i in dom f1
by FINSEQ_1:def 3;
A24:
dom f1 c= dom f
by A5, FINSEQ_1:26;
f /. i =
f . i
by A24, A23, PARTFUN1:def 6
.=
f1 . i
by A5, A23, FINSEQ_1:def 7
.=
f1 /. i
by A23, PARTFUN1:def 6
;
hence
f1 /. i is
with_endpoints
by A22, A21, A8;
verum
end;
per cases
( len f1 = 0 or not len f1 = 0 )
;
suppose
len f1 = 0
;
ex c being with_endpoints Curve of T st
( Sum f = c & dom c = [.(inf (dom (f /. 1))),(sup (dom (f /. (len f)))).] & the_first_point_of c = (f /. 1) . (inf (dom (f /. 1))) & the_last_point_of c = (f /. (len f)) . (sup (dom (f /. (len f)))) )then
f1 = {}
;
then A25:
f = <*c2*>
by A5, FINSEQ_1:34;
take
c2
;
( Sum f = c2 & dom c2 = [.(inf (dom (f /. 1))),(sup (dom (f /. (len f)))).] & the_first_point_of c2 = (f /. 1) . (inf (dom (f /. 1))) & the_last_point_of c2 = (f /. (len f)) . (sup (dom (f /. (len f)))) )
1
in Seg 1
by FINSEQ_1:3;
then A26:
1
in dom f
by A25, FINSEQ_1:38;
A27:
f /. 1 =
f . 1
by A26, PARTFUN1:def 6
.=
c2
by A25, FINSEQ_1:40
;
A28:
f /. (len f) = c2
by A27, A25, FINSEQ_1:40;
thus
(
Sum f = c2 &
dom c2 = [.(inf (dom (f /. 1))),(sup (dom (f /. (len f)))).] &
the_first_point_of c2 = (f /. 1) . (inf (dom (f /. 1))) &
the_last_point_of c2 = (f /. (len f)) . (sup (dom (f /. (len f)))) )
by A25, Th40, A27, A28, Th27;
verum end; suppose A29:
not
len f1 = 0
;
ex c being with_endpoints Curve of T st
( Sum f = c & dom c = [.(inf (dom (f /. 1))),(sup (dom (f /. (len f)))).] & the_first_point_of c = (f /. 1) . (inf (dom (f /. 1))) & the_last_point_of c = (f /. (len f)) . (sup (dom (f /. (len f)))) )consider c1 being
with_endpoints Curve of
T such that A30:
(
Sum f1 = c1 &
dom c1 = [.(inf (dom (f1 /. 1))),(sup (dom (f1 /. (len f1)))).] &
the_first_point_of c1 = (f1 /. 1) . (inf (dom (f1 /. 1))) &
the_last_point_of c1 = (f1 /. (len f1)) . (sup (dom (f1 /. (len f1)))) )
by A4, A6, A11, A20, A3, A29;
set c =
c1 + c2;
A31:
0 + 1
< (len f1) + 1
by A29, XREAL_1:6;
then A32:
1
<= len f1
by NAT_1:13;
A33:
len f1 < len f
by A6, NAT_1:13;
then A34:
(
(f /. (len f1)) . (sup (dom (f /. (len f1)))) = (f /. ((len f1) + 1)) . (inf (dom (f /. ((len f1) + 1)))) &
sup (dom (f /. (len f1))) = inf (dom (f /. ((len f1) + 1))) )
by A32, A7;
(len f1) + 1
in Seg (len f)
by A6, A31, FINSEQ_1:1;
then A35:
(len f1) + 1
in dom f
by FINSEQ_1:def 3;
A36:
f /. ((len f1) + 1) =
f . ((len f1) + 1)
by A35, PARTFUN1:def 6
.=
c2
by A5, FINSEQ_1:42
;
A37:
inf (dom (f1 /. 1)) <= sup (dom (f1 /. (len f1)))
by A30, XXREAL_1:29;
A38:
dom f1 c= dom f
by A5, FINSEQ_1:26;
len f1 in Seg (len f1)
by A29, FINSEQ_1:3;
then A39:
len f1 in dom f1
by FINSEQ_1:def 3;
A40:
f1 /. (len f1) =
f1 . (len f1)
by A39, PARTFUN1:def 6
.=
f . (len f1)
by A5, A39, FINSEQ_1:def 7
.=
f /. (len f1)
by A39, A38, PARTFUN1:def 6
;
A41:
sup (dom c1) = inf (dom c2)
by A36, A34, A40, A30, XXREAL_1:29, XXREAL_2:29;
A42:
the_last_point_of c1 = the_first_point_of c2
by A36, A30, A40, A33, A32, A7;
A43:
(
c1 + c2 is
with_endpoints &
dom (c1 + c2) = [.(inf (dom c1)),(sup (dom c2)).] &
(c1 + c2) . (inf (dom c1)) = the_first_point_of c1 &
(c1 + c2) . (sup (dom c2)) = the_last_point_of c2 )
by A41, A42, Th38;
1
in Seg (len f1)
by A32, FINSEQ_1:1;
then A44:
1
in dom f1
by FINSEQ_1:def 3;
A45:
f1 /. 1 =
f1 . 1
by A44, PARTFUN1:def 6
.=
f . 1
by A44, A5, FINSEQ_1:def 7
.=
f /. 1
by A44, A38, PARTFUN1:def 6
;
reconsider c =
c1 + c2 as
with_endpoints Curve of
T by A41, A42, Th38;
take
c
;
( Sum f = c & dom c = [.(inf (dom (f /. 1))),(sup (dom (f /. (len f)))).] & the_first_point_of c = (f /. 1) . (inf (dom (f /. 1))) & the_last_point_of c = (f /. (len f)) . (sup (dom (f /. (len f)))) )
inf (dom c1) <= sup (dom c2)
by A43, XXREAL_1:29;
hence
(
Sum f = c &
dom c = [.(inf (dom (f /. 1))),(sup (dom (f /. (len f)))).] &
the_first_point_of c = (f /. 1) . (inf (dom (f /. 1))) &
the_last_point_of c = (f /. (len f)) . (sup (dom (f /. (len f)))) )
by A43, A45, A37, A30, A5, Th41, A36, A6, XXREAL_2:25, XXREAL_2:29;
verum end; end;
end;
for k being Nat holds S1[k]
from NAT_1:sch 2(A1, A2);
hence
for f being FinSequence of Curves T st len f > 0 & ( for i being Nat st 1 <= i & i < len f holds
( (f /. i) . (sup (dom (f /. i))) = (f /. (i + 1)) . (inf (dom (f /. (i + 1)))) & sup (dom (f /. i)) = inf (dom (f /. (i + 1))) ) ) & ( for i being Nat st 1 <= i & i <= len f holds
f /. i is with_endpoints ) holds
ex c being with_endpoints Curve of T st
( Sum f = c & dom c = [.(inf (dom (f /. 1))),(sup (dom (f /. (len f)))).] & the_first_point_of c = (f /. 1) . (inf (dom (f /. 1))) & the_last_point_of c = (f /. (len f)) . (sup (dom (f /. (len f)))) )
; verum