set G = Funcs (X,ExtREAL);

per cases ( F is without_+infty-valued or F is without_-infty-valued ) by DEF12;

suppose a1: F is without_+infty-valued ; :: thesis: ex b₁ being FinSequence of Funcs (X,ExtREAL) st
( len F = len b₁ & F . 1 = b₁ . 1 & ( for n being Nat st 1 <= n & n < len F holds
b₁ . (n + 1) = (b₁ /. n) + (F /. (n + 1)) ) )

per cases ( len F > 0 or len F <= 0 ) ;

suppose len F > 0 ; :: thesis: ex b₁ being FinSequence of Funcs (X,ExtREAL) st
( len F = len b₁ & F . 1 = b₁ . 1 & ( for n being Nat st 1 <= n & n < len F holds
b₁ . (n + 1) = (b₁ /. n) + (F /. (n + 1)) ) )

then a2: 0 + 1 <= len F by NAT_1:13;
then a3: 1 in dom F by FINSEQ_3:25;

now :: thesis: for n being Nat st n in dom <*(F /. 1)*> holds
<*(F /. 1)*> . n is without+infty

let n be Nat; :: thesis: ( n in dom <*(F /. 1)*> implies <*(F /. 1)*> . n is without+infty )
assume n in dom <*(F /. 1)*> ; :: thesis: <*(F /. 1)*> . n is without+infty
then n in Seg 1 by FINSEQ_1:38;
then n = 1 by FINSEQ_1:2, TARSKI:def 1;
then <*(F /. 1)*> . n = F /. 1 ;
then <*(F /. 1)*> . n = F . 1 by a3, PARTFUN1:def 6;
hence <*(F /. 1)*> . n is without+infty by a1, a2, FINSEQ_3:25; :: thesis: verum

end;

then reconsider q = <*(F /. 1)*> as without_+infty-valued FinSequence of Funcs (X,ExtREAL) by DEF10;
F /. 1 = F . 1 by a2, FINSEQ_4:15;
then A3: q . 1 = F . 1 ;
defpred S₁[ Nat] means ( $1 + 1 <= len F implies ex g being without_+infty-valued FinSequence of Funcs (X,ExtREAL) st
( $1 + 1 = len g & F . 1 = g . 1 & ( for i being Nat st 1 <= i & i < $1 + 1 holds
g . (i + 1) = (g /. i) + (F /. (i + 1)) ) ) );
A4: for i being Nat st 1 <= i & i < 0 + 1 holds
q . (i + 1) = (q /. i) + (F /. (i + 1)) ;
A5: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A6: S₁[k] ; :: thesis: S₁[k + 1]

per cases ( (k + 1) + 1 <= len F or (k + 1) + 1 > len F ) ;

suppose A7: (k + 1) + 1 <= len F ; :: thesis: S₁[k + 1]

k + 1 < (k + 1) + 1 by XREAL_1:29;
then consider g being without_+infty-valued FinSequence of Funcs (X,ExtREAL) such that
A8: k + 1 = len g and
A9: F . 1 = g . 1 and
A10: for i being Nat st 1 <= i & i < k + 1 holds
g . (i + 1) = (g /. i) + (F /. (i + 1)) by A6, A7, XXREAL_0:2;
A11: 1 <= (k + 1) + 1 by NAT_1:12;
then A12: (F /. ((k + 1) + 1)) " {+infty} = {} by a1, A7, Th53, FINSEQ_3:25;
1 <= k + 1 by NAT_1:12;
then A13: k + 1 in dom g by A8, FINSEQ_3:25;
then (g /. (k + 1)) " {+infty} = {} by Th53;
then ((dom (g /. (k + 1))) /\ (dom (F /. ((k + 1) + 1)))) \ ((((g /. (k + 1)) " {-infty}) /\ ((F /. ((k + 1) + 1)) " {+infty})) \/ (((g /. (k + 1)) " {+infty}) /\ ((F /. ((k + 1) + 1)) " {-infty}))) = (dom (g /. (k + 1))) /\ (dom (F /. ((k + 1) + 1))) by A12;
then A14: dom ((g /. (k + 1)) + (F /. ((k + 1) + 1))) = (dom (g /. (k + 1))) /\ (dom (F /. ((k + 1) + 1))) by MESFUNC1:def 3;
( dom (g /. (k + 1)) = X & dom (F /. ((k + 1) + 1)) = X ) by FUNCT_2:def 1;
then (g /. (k + 1)) + (F /. ((k + 1) + 1)) is Function of X,ExtREAL by A14, FUNCT_2:def 1;
then (g /. (k + 1)) + (F /. ((k + 1) + 1)) is Element of Funcs (X,ExtREAL) by FUNCT_2:8;
then <*((g /. (k + 1)) + (F /. ((k + 1) + 1)))*> is FinSequence of Funcs (X,ExtREAL) by FINSEQ_1:74;
then reconsider g2 = g ^ <*((g /. (k + 1)) + (F /. ((k + 1) + 1)))*> as FinSequence of Funcs (X,ExtREAL) by FINSEQ_1:75;

now :: thesis: for n being Nat st n in dom g2 holds
g2 . n is without+infty

let n be Nat; :: thesis: ( n in dom g2 implies g2 . b₁ is without+infty )
assume n in dom g2 ; :: thesis: g2 . b₁ is without+infty
then A15: ( 1 <= n & n <= len g2 ) by FINSEQ_3:25;
then A16: ( 1 <= n & n <= (len g) + 1 ) by FINSEQ_2:16;

per cases ( n = (len g) + 1 or n <> (len g) + 1 ) ;

suppose A17: n = (len g) + 1 ; :: thesis: g2 . b₁ is without+infty

len <*((g /. (k + 1)) + (F /. ((k + 1) + 1)))*> = 1 by FINSEQ_1:40;
then 1 in dom <*((g /. (k + 1)) + (F /. ((k + 1) + 1)))*> by FINSEQ_3:25;
then A18: g2 . n = <*((g /. (k + 1)) + (F /. ((k + 1) + 1)))*> . 1 by A17, FINSEQ_1:def 7;
A19: (k + 1) + 1 in dom F by A7, NAT_1:12, FINSEQ_3:25;
( g . (k + 1) is without+infty & F . ((k + 1) + 1) is without+infty ) by a1, A13, A11, A7, DEF10, FINSEQ_3:25;
then reconsider p = g /. (k + 1), q = F /. ((k + 1) + 1) as without+infty Function of X,ExtREAL by A13, A19, PARTFUN1:def 6;
p + q is without+infty Function of X,ExtREAL ;
hence g2 . n is without+infty by A18; :: thesis: verum

end;

suppose n <> (len g) + 1 ; :: thesis: g2 . b₁ is without+infty

then n < (len g) + 1 by A16, XXREAL_0:1;
then n <= len g by NAT_1:13;
then A20: n in dom g by A15, FINSEQ_3:25;
then g2 . n = g . n by FINSEQ_1:def 7;
hence g2 . n is without+infty by A20, DEF10; :: thesis: verum

end;

end;

end;

then reconsider g2 = g2 as without_+infty-valued FinSequence of Funcs (X,ExtREAL) by DEF10;
A21: Seg (len g) = dom g by FINSEQ_1:def 3;
A22: len g2 = (len g) + (len <*((g /. (k + 1)) + (F /. ((k + 1) + 1)))*>) by FINSEQ_1:22
.= (k + 1) + 1 by A8, FINSEQ_1:40 ;
A23: for i being Nat st 1 <= i & i < (k + 1) + 1 holds
g2 . (i + 1) = (g2 /. i) + (F /. (i + 1))

proof

let i be Nat; :: thesis: ( 1 <= i & i < (k + 1) + 1 implies g2 . (i + 1) = (g2 /. i) + (F /. (i + 1)) )
A28: 1 <= i + 1 by NAT_1:12;
assume that
A24: 1 <= i and
A25: i < (k + 1) + 1 ; :: thesis: g2 . (i + 1) = (g2 /. i) + (F /. (i + 1))
A26: i <= k + 1 by A25, NAT_1:13;

per cases ( i < k + 1 or i = k + 1 ) by A26, XXREAL_0:1;

suppose A27: i < k + 1 ; :: thesis: g2 . (i + 1) = (g2 /. i) + (F /. (i + 1))

then i + 1 <= k + 1 by NAT_1:13;
then i + 1 in Seg (len g) by A8, A28;
then A29: g2 . (i + 1) = g . (i + 1) by A21, FINSEQ_1:def 7;
i in Seg (len g) by A8, A24, A26;
then A30: g2 . i = g . i by A21, FINSEQ_1:def 7;
A31: g /. i = g . i by A8, A24, A27, FINSEQ_4:15;
g2 /. i = g2 . i by A22, A24, A25, FINSEQ_4:15;
hence g2 . (i + 1) = (g2 /. i) + (F /. (i + 1)) by A10, A24, A27, A29, A30, A31; :: thesis: verum

end;

suppose A32: i = k + 1 ; :: thesis: g2 . (i + 1) = (g2 /. i) + (F /. (i + 1))

A33: g2 /. i = g2 . i by A22, A24, A25, FINSEQ_4:15;
i in Seg (len g) by A8, A24, A26;
then A34: g . i = g2 . i by A21, FINSEQ_1:def 7;
g /. i = g . i by A8, A24, A26, FINSEQ_4:15;
hence g2 . (i + 1) = (g2 /. i) + (F /. (i + 1)) by A8, A32, A34, A33, FINSEQ_1:42; :: thesis: verum

end;

end;

end;

1 <= k + 1 by NAT_1:11;
then 1 in Seg (len g) by A8;
then g2 . 1 = F . 1 by A9, A21, FINSEQ_1:def 7;
hence S₁[k + 1] by A22, A23; :: thesis: verum

end;

suppose (k + 1) + 1 > len F ; :: thesis: S₁[k + 1]

hence S₁[k + 1] ; :: thesis: verum

end;

end;

end;

A35: (len F) -' 1 = (len F) - 1 by a2, XREAL_1:233;
len q = 1 by FINSEQ_1:40;
then A36: S₁[ 0 ] by A3, A4;
for k being Nat holds S₁[k] from NAT_1:sch 2(A36, A5);
then ex IT being without_+infty-valued FinSequence of Funcs (X,ExtREAL) st
( ((len F) -' 1) + 1 = len IT & F . 1 = IT . 1 & ( for i being Nat st 1 <= i & i < ((len F) -' 1) + 1 holds
IT . (i + 1) = (IT /. i) + (F /. (i + 1)) ) ) by A35;
hence ex IT being FinSequence of Funcs (X,ExtREAL) st
( len F = len IT & F . 1 = IT . 1 & ( for n being Nat st 1 <= n & n < len F holds
IT . (n + 1) = (IT /. n) + (F /. (n + 1)) ) ) by A35; :: thesis: verum

end;

suppose A37: len F <= 0 ; :: thesis: ex b₁ being FinSequence of Funcs (X,ExtREAL) st
( len F = len b₁ & F . 1 = b₁ . 1 & ( for n being Nat st 1 <= n & n < len F holds
b₁ . (n + 1) = (b₁ /. n) + (F /. (n + 1)) ) )

take F ; :: thesis: ( len F = len F & F . 1 = F . 1 & ( for n being Nat st 1 <= n & n < len F holds
F . (n + 1) = (F /. n) + (F /. (n + 1)) ) )
thus ( len F = len F & F . 1 = F . 1 ) ; :: thesis: for n being Nat st 1 <= n & n < len F holds
F . (n + 1) = (F /. n) + (F /. (n + 1))
let n be Nat; :: thesis: ( 1 <= n & n < len F implies F . (n + 1) = (F /. n) + (F /. (n + 1)) )
thus ( 1 <= n & n < len F implies F . (n + 1) = (F /. n) + (F /. (n + 1)) ) by A37; :: thesis: verum

end;

end;

end;

suppose A38: F is without_-infty-valued ; :: thesis: ex b₁ being FinSequence of Funcs (X,ExtREAL) st
( len F = len b₁ & F . 1 = b₁ . 1 & ( for n being Nat st 1 <= n & n < len F holds
b₁ . (n + 1) = (b₁ /. n) + (F /. (n + 1)) ) )

per cases ( len F > 0 or len F <= 0 ) ;

suppose A39: len F > 0 ; :: thesis: ex b₁ being FinSequence of Funcs (X,ExtREAL) st
( len F = len b₁ & F . 1 = b₁ . 1 & ( for n being Nat st 1 <= n & n < len F holds
b₁ . (n + 1) = (b₁ /. n) + (F /. (n + 1)) ) )

then A40: 0 + 1 <= len F by NAT_1:13;
then A41: 1 in dom F by FINSEQ_3:25;

now :: thesis: for n being Nat st n in dom <*(F /. 1)*> holds
<*(F /. 1)*> . n is without-infty

let n be Nat; :: thesis: ( n in dom <*(F /. 1)*> implies <*(F /. 1)*> . n is without-infty )
assume n in dom <*(F /. 1)*> ; :: thesis: <*(F /. 1)*> . n is without-infty
then n in Seg 1 by FINSEQ_1:38;
then n = 1 by FINSEQ_1:2, TARSKI:def 1;
then <*(F /. 1)*> . n = F /. 1 ;
then <*(F /. 1)*> . n = F . 1 by A41, PARTFUN1:def 6;
hence <*(F /. 1)*> . n is without-infty by A38, A40, FINSEQ_3:25; :: thesis: verum

end;

then reconsider q = <*(F /. 1)*> as without_-infty-valued FinSequence of Funcs (X,ExtREAL) by DEF11;
A42: 0 + 1 <= len F by A39, NAT_1:13;
then F /. 1 = F . 1 by FINSEQ_4:15;
then A43: q . 1 = F . 1 ;
defpred S₁[ Nat] means ( $1 + 1 <= len F implies ex g being without_-infty-valued FinSequence of Funcs (X,ExtREAL) st
( $1 + 1 = len g & F . 1 = g . 1 & ( for i being Nat st 1 <= i & i < $1 + 1 holds
g . (i + 1) = (g /. i) + (F /. (i + 1)) ) ) );
A44: for i being Nat st 1 <= i & i < 0 + 1 holds
q . (i + 1) = (q /. i) + (F /. (i + 1)) ;
A45: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A46: S₁[k] ; :: thesis: S₁[k + 1]

per cases ( (k + 1) + 1 <= len F or (k + 1) + 1 > len F ) ;

suppose A47: (k + 1) + 1 <= len F ; :: thesis: S₁[k + 1]

k + 1 < (k + 1) + 1 by XREAL_1:29;
then consider g being without_-infty-valued FinSequence of Funcs (X,ExtREAL) such that
A48: k + 1 = len g and
A49: F . 1 = g . 1 and
A50: for i being Nat st 1 <= i & i < k + 1 holds
g . (i + 1) = (g /. i) + (F /. (i + 1)) by A46, A47, XXREAL_0:2;
A51: (k + 1) + 1 in dom F by A47, NAT_1:12, FINSEQ_3:25;
then A52: (F /. ((k + 1) + 1)) " {-infty} = {} by A38, Th54;
1 <= k + 1 by NAT_1:12;
then A53: k + 1 in dom g by A48, FINSEQ_3:25;
then (g /. (k + 1)) " {-infty} = {} by Th54;
then ((dom (g /. (k + 1))) /\ (dom (F /. ((k + 1) + 1)))) \ ((((g /. (k + 1)) " {-infty}) /\ ((F /. ((k + 1) + 1)) " {+infty})) \/ (((g /. (k + 1)) " {+infty}) /\ ((F /. ((k + 1) + 1)) " {-infty}))) = (dom (g /. (k + 1))) /\ (dom (F /. ((k + 1) + 1))) by A52;
then A54: dom ((g /. (k + 1)) + (F /. ((k + 1) + 1))) = (dom (g /. (k + 1))) /\ (dom (F /. ((k + 1) + 1))) by MESFUNC1:def 3;
( dom (g /. (k + 1)) = X & dom (F /. ((k + 1) + 1)) = X ) by FUNCT_2:def 1;
then (g /. (k + 1)) + (F /. ((k + 1) + 1)) is Function of X,ExtREAL by A54, FUNCT_2:def 1;
then (g /. (k + 1)) + (F /. ((k + 1) + 1)) is Element of Funcs (X,ExtREAL) by FUNCT_2:8;
then <*((g /. (k + 1)) + (F /. ((k + 1) + 1)))*> is FinSequence of Funcs (X,ExtREAL) by FINSEQ_1:74;
then reconsider g2 = g ^ <*((g /. (k + 1)) + (F /. ((k + 1) + 1)))*> as FinSequence of Funcs (X,ExtREAL) by FINSEQ_1:75;

now :: thesis: for n being Nat st n in dom g2 holds
g2 . n is without-infty

let n be Nat; :: thesis: ( n in dom g2 implies g2 . b₁ is without-infty )
assume n in dom g2 ; :: thesis: g2 . b₁ is without-infty
then A55: ( 1 <= n & n <= len g2 ) by FINSEQ_3:25;
then A56: ( 1 <= n & n <= (len g) + 1 ) by FINSEQ_2:16;

per cases ( n = (len g) + 1 or n <> (len g) + 1 ) ;

suppose A57: n = (len g) + 1 ; :: thesis: g2 . b₁ is without-infty

len <*((g /. (k + 1)) + (F /. ((k + 1) + 1)))*> = 1 by FINSEQ_1:40;
then 1 in dom <*((g /. (k + 1)) + (F /. ((k + 1) + 1)))*> by FINSEQ_3:25;
then A58: g2 . n = <*((g /. (k + 1)) + (F /. ((k + 1) + 1)))*> . 1 by A57, FINSEQ_1:def 7;
( g . (k + 1) is without-infty & F . ((k + 1) + 1) is without-infty ) by A38, A51, A53, DEF11;
then reconsider p = g /. (k + 1), q = F /. ((k + 1) + 1) as without-infty Function of X,ExtREAL by A51, A53, PARTFUN1:def 6;
p + q is without-infty Function of X,ExtREAL ;
hence g2 . n is without-infty by A58; :: thesis: verum

end;

suppose n <> (len g) + 1 ; :: thesis: g2 . b₁ is without-infty

then n < (len g) + 1 by A56, XXREAL_0:1;
then n <= len g by NAT_1:13;
then A59: n in dom g by A55, FINSEQ_3:25;
then g2 . n = g . n by FINSEQ_1:def 7;
hence g2 . n is without-infty by A59, DEF11; :: thesis: verum

end;

end;

end;

then reconsider g2 = g2 as without_-infty-valued FinSequence of Funcs (X,ExtREAL) by DEF11;
A60: Seg (len g) = dom g by FINSEQ_1:def 3;
A61: len g2 = (len g) + (len <*((g /. (k + 1)) + (F /. ((k + 1) + 1)))*>) by FINSEQ_1:22
.= (k + 1) + 1 by A48, FINSEQ_1:40 ;
A62: for i being Nat st 1 <= i & i < (k + 1) + 1 holds
g2 . (i + 1) = (g2 /. i) + (F /. (i + 1))

proof

let i be Nat; :: thesis: ( 1 <= i & i < (k + 1) + 1 implies g2 . (i + 1) = (g2 /. i) + (F /. (i + 1)) )
assume A63: ( 1 <= i & i < (k + 1) + 1 ) ; :: thesis: g2 . (i + 1) = (g2 /. i) + (F /. (i + 1))
then A65: i <= k + 1 by NAT_1:13;

per cases ( i < k + 1 or i = k + 1 ) by A65, XXREAL_0:1;

suppose A66: i < k + 1 ; :: thesis: g2 . (i + 1) = (g2 /. i) + (F /. (i + 1))

A67: 1 <= i + 1 by NAT_1:12;
i + 1 <= k + 1 by A66, NAT_1:13;
then i + 1 in Seg (len g) by A48, A67;
then A68: g2 . (i + 1) = g . (i + 1) by A60, FINSEQ_1:def 7;
i in Seg (len g) by A48, A63, A65;
then A69: g2 . i = g . i by A60, FINSEQ_1:def 7;
A70: g /. i = g . i by A48, A63, A66, FINSEQ_4:15;
g2 /. i = g2 . i by A61, A63, FINSEQ_4:15;
hence g2 . (i + 1) = (g2 /. i) + (F /. (i + 1)) by A50, A63, A66, A68, A69, A70; :: thesis: verum

end;

suppose A71: i = k + 1 ; :: thesis: g2 . (i + 1) = (g2 /. i) + (F /. (i + 1))

A72: g2 /. i = g2 . i by A61, A63, FINSEQ_4:15;
i in Seg (len g) by A48, A63, A65;
then A73: g . i = g2 . i by A60, FINSEQ_1:def 7;
g /. i = g . i by A48, A63, A65, FINSEQ_4:15;
hence g2 . (i + 1) = (g2 /. i) + (F /. (i + 1)) by A48, A71, A72, A73, FINSEQ_1:42; :: thesis: verum

end;

end;

end;

1 <= k + 1 by NAT_1:11;
then 1 in Seg (len g) by A48;
then g2 . 1 = F . 1 by A49, A60, FINSEQ_1:def 7;
hence S₁[k + 1] by A61, A62; :: thesis: verum

end;

suppose (k + 1) + 1 > len F ; :: thesis: S₁[k + 1]

hence S₁[k + 1] ; :: thesis: verum

end;

end;

end;

A74: (len F) -' 1 = (len F) - 1 by A42, XREAL_1:233;
len q = 1 by FINSEQ_1:40;
then A75: S₁[ 0 ] by A43, A44;
for k being Nat holds S₁[k] from NAT_1:sch 2(A75, A45);
then ex IT being without_-infty-valued FinSequence of Funcs (X,ExtREAL) st
( ((len F) -' 1) + 1 = len IT & F . 1 = IT . 1 & ( for i being Nat st 1 <= i & i < ((len F) -' 1) + 1 holds
IT . (i + 1) = (IT /. i) + (F /. (i + 1)) ) ) by A74;
hence ex IT being FinSequence of Funcs (X,ExtREAL) st
( len F = len IT & F . 1 = IT . 1 & ( for n being Nat st 1 <= n & n < len F holds
IT . (n + 1) = (IT /. n) + (F /. (n + 1)) ) ) by A74; :: thesis: verum

end;

suppose A76: len F <= 0 ; :: thesis: ex b₁ being FinSequence of Funcs (X,ExtREAL) st
( len F = len b₁ & F . 1 = b₁ . 1 & ( for n being Nat st 1 <= n & n < len F holds
b₁ . (n + 1) = (b₁ /. n) + (F /. (n + 1)) ) )

take F ; :: thesis: ( len F = len F & F . 1 = F . 1 & ( for n being Nat st 1 <= n & n < len F holds
F . (n + 1) = (F /. n) + (F /. (n + 1)) ) )
thus ( len F = len F & F . 1 = F . 1 ) ; :: thesis: for n being Nat st 1 <= n & n < len F holds
F . (n + 1) = (F /. n) + (F /. (n + 1))
let n be Nat; :: thesis: ( 1 <= n & n < len F implies F . (n + 1) = (F /. n) + (F /. (n + 1)) )
thus ( 1 <= n & n < len F implies F . (n + 1) = (F /. n) + (F /. (n + 1)) ) by A76; :: thesis: verum

end;

end;

end;

end;