let T be non empty TopStruct ; :: thesis: for X being set
for f being FinSequence of Curves T st ( for i being Nat st 1 <= i & i <= len f holds
rng (f /. i) c= X ) holds
rng (Sum f) c= X
let X be set ; :: thesis: for f being FinSequence of Curves T st ( for i being Nat st 1 <= i & i <= len f holds
rng (f /. i) c= X ) holds
rng (Sum f) c= X
defpred S₁[ Nat] means for f being FinSequence of Curves T st len f = $1 & ( for i being Nat st 1 <= i & i <= len f holds
rng (f /. i) c= X ) holds
rng (Sum f) c= X;
A1: S₁[ 0 ]

proof

let f be FinSequence of Curves T; :: thesis: ( len f = 0 & ( for i being Nat st 1 <= i & i <= len f holds
rng (f /. i) c= X ) implies rng (Sum f) c= X )
assume len f = 0 ; :: thesis: ( ex i being Nat st
( 1 <= i & i <= len f & not rng (f /. i) c= X ) or rng (Sum f) c= X )
then Sum f = {} by Def14;
then rng (Sum f) = {} ;
hence ( ex i being Nat st
( 1 <= i & i <= len f & not rng (f /. i) c= X ) or rng (Sum f) c= X ) ; :: thesis: verum

end;

A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
let f be FinSequence of Curves T; :: thesis: ( len f = k + 1 & ( for i being Nat st 1 <= i & i <= len f holds
rng (f /. i) c= X ) implies rng (Sum f) c= X )
assume A4: len f = k + 1 ; :: thesis: ( ex i being Nat st
( 1 <= i & i <= len f & not rng (f /. i) c= X ) or rng (Sum f) c= X )
then consider f1 being FinSequence of Curves T, c being Element of Curves T such that
A5: f = f1 ^ <*c*> by FINSEQ_2:19;
assume A6: for i being Nat st 1 <= i & i <= len f holds
rng (f /. i) c= X ; :: thesis: rng (Sum f) c= X
A7: len f = (len f1) + (len <*c*>) by A5, FINSEQ_1:22
.= (len f1) + 1 by FINSEQ_1:39 ;
A8: Sum f = (Sum f1) + c by A5, Th41;

per cases ( not (Sum f1) \/ c is Curve of T or (Sum f1) \/ c is Curve of T ) ;

suppose (Sum f1) \/ c is not Curve of T ; :: thesis: rng (Sum f) c= X

then Sum f = {} by A8, Def12;
then rng (Sum f) = {} ;
hence rng (Sum f) c= X ; :: thesis: verum

end;

suppose (Sum f1) \/ c is Curve of T ; :: thesis: rng (Sum f) c= X

then A9: Sum f = (Sum f1) \/ c by A8, Def12;
A10: for i being Nat st 1 <= i & i <= len f1 holds
rng (f1 /. i) c= X

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len f1 implies rng (f1 /. i) c= X )
assume A11: ( 1 <= i & i <= len f1 ) ; :: thesis: rng (f1 /. i) c= X
then A12: i + 1 <= (len f1) + 1 by XREAL_1:6;
i <= i + 1 by NAT_1:12;
then A13: i <= len f by A12, A7, XXREAL_0:2;
then A14: rng (f /. i) c= X by A6, A11;
i in Seg (len f) by A11, A13, FINSEQ_1:1;
then i in dom f by FINSEQ_1:def 3;
then A15: rng (f . i) c= X by A14, PARTFUN1:def 6;
i in Seg (len f1) by A11, FINSEQ_1:1;
then A16: i in dom f1 by FINSEQ_1:def 3;
then f . i = f1 . i by A5, FINSEQ_1:def 7;
hence rng (f1 /. i) c= X by A15, A16, PARTFUN1:def 6; :: thesis: verum

end;

A17: rng (Sum f1) c= X by A3, A7, A4, A10;
len f in Seg (len f) by A7, FINSEQ_1:3;
then A18: len f in dom f by FINSEQ_1:def 3;
f . (len f) = c by A7, A5, FINSEQ_1:42;
then A19: f /. (len f) = c by A18, PARTFUN1:def 6;
0 + 1 <= (len f1) + 1 by XREAL_1:6;
then A20: rng c c= X by A7, A19, A6;
rng (Sum f) = (rng (Sum f1)) \/ (rng c) by A9, RELAT_1:12;
hence rng (Sum f) c= X by A17, A20, XBOOLE_1:8; :: thesis: verum

end;

end;

end;

A21: for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A2);
let f be FinSequence of Curves T; :: thesis: ( ( for i being Nat st 1 <= i & i <= len f holds
rng (f /. i) c= X ) implies rng (Sum f) c= X )
thus ( ( for i being Nat st 1 <= i & i <= len f holds
rng (f /. i) c= X ) implies rng (Sum f) c= X ) by A21; :: thesis: verum