let n be Nat; :: thesis: for g being FinSequence of REAL n
for h being FinSequence of NAT
for F being FinSequence of REAL n st h is increasing & rng h c= dom g & F = g * h & ( for i being Element of NAT st i in dom g & not i in rng h holds
g . i = 0* n ) holds
Sum g = Sum F
let g be FinSequence of REAL n; :: thesis: for h being FinSequence of NAT
for F being FinSequence of REAL n st h is increasing & rng h c= dom g & F = g * h & ( for i being Element of NAT st i in dom g & not i in rng h holds
g . i = 0* n ) holds
Sum g = Sum F
let h be FinSequence of NAT ; :: thesis: for F being FinSequence of REAL n st h is increasing & rng h c= dom g & F = g * h & ( for i being Element of NAT st i in dom g & not i in rng h holds
g . i = 0* n ) holds
Sum g = Sum F
let F be FinSequence of REAL n; :: thesis: ( h is increasing & rng h c= dom g & F = g * h & ( for i being Element of NAT st i in dom g & not i in rng h holds
g . i = 0* n ) implies Sum g = Sum F )
assume that
A1: h is increasing and
A2: rng h c= dom g and
A3: F = g * h and
A4: for i being Element of NAT st i in dom g & not i in rng h holds
g . i = 0* n ; :: thesis: Sum g = Sum F
A5: dom (h * g) = dom h by A2, RELAT_1:27;
dom (g * h) = dom h by A2, RELAT_1:27;
then A6: dom F = Seg (len h) by A3, FINSEQ_1:def 3;
then A7: len F = len h by FINSEQ_1:def 3;
dom h c= dom g
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom h or x in dom g )
assume A8: x in dom h ; :: thesis: x in dom g
then reconsider nx = x as Element of NAT ;
A9: h . x in rng h by A8, FUNCT_1:def 3;
then reconsider nhx = h . x as Element of NAT ;
A10: nx in Seg (len h) by A8, FINSEQ_1:def 3;
then A11: 1 <= nx by FINSEQ_1:1;
A12: nx <= len h by A10, FINSEQ_1:1;
then 1 <= len h by A11, XXREAL_0:2;
then 1 in Seg (len h) by FINSEQ_1:1;
then 1 in dom h by FINSEQ_1:def 3;
then h . 1 in rng h by FUNCT_1:def 3;
then h . 1 in dom g by A2;
then h . 1 in Seg (len g) by FINSEQ_1:def 3;
then 1 <= h . 1 by FINSEQ_1:1;
then A13: nx <= nhx by A1, A12, Th7;
h . x in dom g by A2, A9;
then h . x in Seg (len g) by FINSEQ_1:def 3;
then nhx <= len g by FINSEQ_1:1;
then nx <= len g by A13, XXREAL_0:2;
then nx in Seg (len g) by A11, FINSEQ_1:1;
hence x in dom g by FINSEQ_1:def 3; :: thesis: verum
end;
then dom h c= Seg (len g) by FINSEQ_1:def 3;
then Seg (len h) c= Seg (len g) by FINSEQ_1:def 3;
then A14: len h <= len g by FINSEQ_1:5;
per cases ( len F > 0 or len F <= 0 ) ;
suppose A15: len F > 0 ; :: thesis: Sum g = Sum F
then A16: 0 + 1 <= len F by NAT_1:13;
then 1 in Seg (len F) by FINSEQ_1:1;
then A17: 1 in dom F by FINSEQ_1:def 3;
then A18: 1 in Seg (len h) by A3, A5, FINSEQ_1:def 3;
then A19: 1 <= len h by FINSEQ_1:1;
then len h in Seg (len h) by FINSEQ_1:1;
then len h in dom h by FINSEQ_1:def 3;
then h . (len h) in rng h by FUNCT_1:def 3;
then h . (len h) in dom g by A2;
then A20: h . (len h) in Seg (len g) by FINSEQ_1:def 3;
reconsider j = h . 1 as Nat ;
dom (h * g) = dom h by A2, RELAT_1:27;
then A21: Seg (len F) = dom h by A3, FINSEQ_1:def 3;
then A22: len F = len h by FINSEQ_1:def 3;
A23: h . 1 in rng h by A3, A5, A17, FUNCT_1:def 3;
then A24: h . 1 in dom g by A2;
then A25: h . 1 in Seg (len g) by FINSEQ_1:def 3;
then A26: 1 <= h . 1 by FINSEQ_1:1;
then A27: j -' 1 = j - 1 by XREAL_1:233;
Seg (len g) <> {} by A2, A23, FINSEQ_1:def 3;
then 0 < len g ;
then A28: 0 + 1 <= len g by NAT_1:13;
then A29: (len g) -' 1 = (len g) - 1 by XREAL_1:233;
then A30: h . (len h) <= ((len g) -' 1) + 1 by A20, FINSEQ_1:1;
A31: 1 <= j by A25, FINSEQ_1:1;
set g4 = accum g;
A32: len g = len (accum g) by Def10;
A33: g . 1 = (accum g) . 1 by Def10;
A34: for i being Nat st 1 <= i & i < len g holds
(accum g) . (i + 1) = ((accum g) /. i) + (g /. (i + 1)) by Def10;
A35: Sum g = (accum g) . (len g) by A7, A14, A15, Def11;
set g2 = accum F;
A36: len F = len (accum F) by Def10;
A37: F . 1 = (accum F) . 1 by Def10;
A38: for i being Nat st 1 <= i & i < len F holds
(accum F) . (i + 1) = ((accum F) /. i) + (F /. (i + 1)) by Def10;
A39: Sum F = (accum F) . (len F) by A15, Def11;
defpred S1[ Nat] means ( 1 <= $1 + 1 & $1 + 1 < j implies (accum g) . ($1 + 1) = 0* n );
A40: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A41: S1[k] ; :: thesis: S1[k + 1]
( 1 <= (k + 1) + 1 & (k + 1) + 1 < j implies (accum g) . ((k + 1) + 1) = 0* n )
proof
assume that
A42: 1 <= (k + 1) + 1 and
A43: (k + 1) + 1 < j ; :: thesis: (accum g) . ((k + 1) + 1) = 0* n
per cases ( 1 < (k + 1) + 1 or 1 = (k + 1) + 1 ) by A42, XXREAL_0:1;
suppose A44: 1 < (k + 1) + 1 ; :: thesis: (accum g) . ((k + 1) + 1) = 0* n
j in Seg (len g) by A24, FINSEQ_1:def 3;
then A45: j <= len g by FINSEQ_1:1;
then (k + 1) + 1 < len g by A43, XXREAL_0:2;
then A46: g /. ((k + 1) + 1) = g . ((k + 1) + 1) by A44, FINSEQ_4:15;
A47: now :: thesis: not (k + 1) + 1 in rng h
assume (k + 1) + 1 in rng h ; :: thesis: contradiction
then consider x0 being object such that
A48: x0 in dom h and
A49: h . x0 = (k + 1) + 1 by FUNCT_1:def 3;
reconsider nx0 = x0 as Element of NAT by A48;
A50: x0 in Seg (len h) by A48, FINSEQ_1:def 3;
then A51: nx0 <= len h by FINSEQ_1:1;
1 <= nx0 by A50, FINSEQ_1:1;
hence contradiction by A1, A43, A49, A51, Th6; :: thesis: verum
end;
A52: k + 1 < (k + 1) + 1 by XREAL_1:29;
then k + 1 < j by A43, XXREAL_0:2;
then A53: k + 1 < len g by A45, XXREAL_0:2;
then A54: (accum g) /. (k + 1) = (accum g) . (k + 1) by A32, FINSEQ_4:15, NAT_1:11;
(k + 1) + 1 <= len g by A53, NAT_1:13;
then (k + 1) + 1 in Seg (len g) by A42, FINSEQ_1:1;
then (k + 1) + 1 in dom g by FINSEQ_1:def 3;
then A55: g . ((k + 1) + 1) = 0* n by A4, A47;
(accum g) . ((k + 1) + 1) = ((accum g) /. (k + 1)) + (g /. ((k + 1) + 1)) by A34, A53, NAT_1:11;
hence (accum g) . ((k + 1) + 1) = 0* n by A41, A43, A52, A55, A54, A46, EUCLID_4:1, NAT_1:11, XXREAL_0:2; :: thesis: verum
end;
suppose 1 = (k + 1) + 1 ; :: thesis: (accum g) . ((k + 1) + 1) = 0* n
hence (accum g) . ((k + 1) + 1) = 0* n ; :: thesis: verum
end;
end;
end;
hence S1[k + 1] ; :: thesis: verum
end;
defpred S2[ Nat] means ( 1 <= $1 + 1 & $1 + 1 <= len (accum F) implies (accum g) . (h . ($1 + 1)) = (accum F) . ($1 + 1) );
A56: 1 in Seg (len g) by A28, FINSEQ_1:1;
( 1 < j implies ( 1 in dom g & not 1 in rng h ) )
proof
assume A57: 1 < j ; :: thesis: ( 1 in dom g & not 1 in rng h )
thus 1 in dom g by A56, FINSEQ_1:def 3; :: thesis: not 1 in rng h
hereby :: thesis: verum
assume 1 in rng h ; :: thesis: contradiction
then consider x0 being object such that
A58: x0 in dom h and
A59: h . x0 = 1 by FUNCT_1:def 3;
reconsider nx0 = x0 as Element of NAT by A58;
A60: x0 in Seg (len h) by A58, FINSEQ_1:def 3;
then A61: nx0 <= len h by FINSEQ_1:1;
1 <= nx0 by A60, FINSEQ_1:1;
hence contradiction by A1, A57, A59, A61, Th6; :: thesis: verum
end;
end;
then A62: S1[ 0 ] by A4, A33;
A63: for k being Nat holds S1[k] from NAT_1:sch 2(A62, A40);
A64: now :: thesis: ( ( 1 < j & S2[ 0 ] ) or ( j = 1 & S2[ 0 ] ) )
per cases ( 1 < j or j = 1 ) by A26, XXREAL_0:1;
case 1 < j ; :: thesis: S2[ 0 ]
then 1 + 1 <= j by NAT_1:13;
then A65: (1 + 1) - 1 <= j - 1 by XREAL_1:9;
then 1 <= j -' 1 by A31, XREAL_1:233;
then A66: ((j -' 1) -' 1) + 1 = ((j -' 1) - 1) + 1 by XREAL_1:233
.= j -' 1 ;
A67: g . j = (accum F) . 1 by A3, A5, A37, A17, FUNCT_1:13;
A68: S1[(j -' 1) -' 1] by A63;
A69: j in Seg (len g) by A24, FINSEQ_1:def 3;
then A70: j <= len g by FINSEQ_1:1;
1 <= j by A69, FINSEQ_1:1;
then A71: g /. j = g . j by A70, FINSEQ_4:15;
A72: (accum F) /. 1 = (accum F) . 1 by A36, A16, FINSEQ_4:15;
A73: j -' 1 < (j -' 1) + 1 by XREAL_1:29;
then A74: j -' 1 < len g by A27, A70, XXREAL_0:2;
then (accum g) /. (j -' 1) = (accum g) . (j -' 1) by A32, A27, A65, FINSEQ_4:15;
then (accum g) . j = (0* n) + ((accum F) /. 1) by Def10, A27, A65, A73, A74, A68, A66, A71, A72, A67
.= (accum F) /. 1 by EUCLID_4:1 ;
hence S2[ 0 ] by FINSEQ_4:15; :: thesis: verum
end;
case j = 1 ; :: thesis: S2[ 0 ]
hence S2[ 0 ] by A3, A5, A37, A33, A17, FUNCT_1:13; :: thesis: verum
end;
end;
end;
A75: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume A76: S2[k] ; :: thesis: S2[k + 1]
( 1 <= (k + 1) + 1 & (k + 1) + 1 <= len (accum F) implies (accum g) . (h . ((k + 1) + 1)) = (accum F) . ((k + 1) + 1) )
proof
defpred S3[ Nat] means ( h . (k + 1) <= $1 + 1 & $1 + 1 < h . ((k + 1) + 1) implies (accum g) . ($1 + 1) = (accum F) . (k + 1) );
assume that
A77: 1 <= (k + 1) + 1 and
A78: (k + 1) + 1 <= len (accum F) ; :: thesis: (accum g) . (h . ((k + 1) + 1)) = (accum F) . ((k + 1) + 1)
A79: (k + 1) + 1 in Seg (len (accum F)) by A77, A78, FINSEQ_1:1;
then h . ((k + 1) + 1) in rng h by A36, A21, FUNCT_1:def 3;
then h . ((k + 1) + 1) in dom g by A2;
then A80: h . ((k + 1) + 1) in Seg (len g) by FINSEQ_1:def 3;
then A81: 1 <= h . ((k + 1) + 1) by FINSEQ_1:1;
A82: k + 1 < (k + 1) + 1 by XREAL_1:29;
then A83: k + 1 < len (accum F) by A78, XXREAL_0:2;
now :: thesis: ( ( 1 <= k & S3[ 0 ] ) or ( k < 1 & S3[ 0 ] ) )
per cases ( 1 <= k or k < 1 ) ;
case k < 1 ; :: thesis: S3[ 0 ]
hence S3[ 0 ] by A15, A36, A64, NAT_1:14; :: thesis: verum
end;
end;
end;
then A87: S3[ 0 ] ;
A88: h . ((k + 1) + 1) <= len g by A80, FINSEQ_1:1;
1 <= k + 1 by NAT_1:11;
then A89: h . (k + 1) < h . ((k + 1) + 1) by A1, A36, A22, A83;
A90: for k2 being Nat st S3[k2] holds
S3[k2 + 1]
proof
let k2 be Nat; :: thesis: ( S3[k2] implies S3[k2 + 1] )
assume A91: S3[k2] ; :: thesis: S3[k2 + 1]
( h . (k + 1) <= (k2 + 1) + 1 & (k2 + 1) + 1 < h . ((k + 1) + 1) implies (accum g) . ((k2 + 1) + 1) = (accum F) . (k + 1) )
proof
assume that
A92: h . (k + 1) <= (k2 + 1) + 1 and
A93: (k2 + 1) + 1 < h . ((k + 1) + 1) ; :: thesis: (accum g) . ((k2 + 1) + 1) = (accum F) . (k + 1)
per cases ( h . (k + 1) < (k2 + 1) + 1 or h . (k + 1) = (k2 + 1) + 1 ) by A92, XXREAL_0:1;
suppose A94: h . (k + 1) < (k2 + 1) + 1 ; :: thesis: (accum g) . ((k2 + 1) + 1) = (accum F) . (k + 1)
A95: now :: thesis: not (k2 + 1) + 1 in rng h
assume (k2 + 1) + 1 in rng h ; :: thesis: contradiction
then consider x0 being object such that
A96: x0 in dom h and
A97: h . x0 = (k2 + 1) + 1 by FUNCT_1:def 3;
reconsider nx0 = x0 as Element of NAT by A96;
A98: x0 in Seg (len h) by A96, FINSEQ_1:def 3;
then nx0 <= len h by FINSEQ_1:1;
then A99: ( nx0 >= (k + 1) + 1 implies h . nx0 >= h . ((k + 1) + 1) ) by A1, A77, Th6;
1 <= nx0 by A98, FINSEQ_1:1;
then ( nx0 <= k + 1 implies h . nx0 <= h . (k + 1) ) by A1, A36, A22, A83, Th6;
hence contradiction by A93, A94, A97, A99, NAT_1:13; :: thesis: verum
end;
h . ((k + 1) + 1) in rng h by A36, A21, A79, FUNCT_1:def 3;
then h . ((k + 1) + 1) in dom g by A2;
then h . ((k + 1) + 1) in Seg (len g) by FINSEQ_1:def 3;
then h . ((k + 1) + 1) <= len g by FINSEQ_1:1;
then A100: (k2 + 1) + 1 < len g by A93, XXREAL_0:2;
A101: 1 < (k2 + 1) + 1 by XREAL_1:29;
then A102: g /. ((k2 + 1) + 1) = g . ((k2 + 1) + 1) by A100, FINSEQ_4:15;
A103: k2 + 1 < (k2 + 1) + 1 by XREAL_1:29;
then A104: k2 + 1 < len g by A100, XXREAL_0:2;
(k2 + 1) + 1 in Seg (len g) by A100, A101, FINSEQ_1:1;
then (k2 + 1) + 1 in dom g by FINSEQ_1:def 3;
then A105: g . ((k2 + 1) + 1) = 0* n by A4, A95;
k2 + 1 < len g by A103, A100, XXREAL_0:2;
then (accum g) . ((k2 + 1) + 1) = ((accum g) /. (k2 + 1)) + (g /. ((k2 + 1) + 1)) by A34, NAT_1:11
.= (accum g) /. (k2 + 1) by A105, A102, EUCLID_4:1
.= (accum g) . (k2 + 1) by A32, A104, FINSEQ_4:15, NAT_1:11 ;
hence (accum g) . ((k2 + 1) + 1) = (accum F) . (k + 1) by A91, A93, A94, NAT_1:13; :: thesis: verum
end;
suppose h . (k + 1) = (k2 + 1) + 1 ; :: thesis: (accum g) . ((k2 + 1) + 1) = (accum F) . (k + 1)
hence (accum g) . ((k2 + 1) + 1) = (accum F) . (k + 1) by A76, A78, A82, NAT_1:11, XXREAL_0:2; :: thesis: verum
end;
end;
end;
hence S3[k2 + 1] ; :: thesis: verum
end;
A106: for k2 being Nat holds S3[k2] from NAT_1:sch 2(A87, A90);
 then A107: ( h . (k + 1) <= (((h . ((k + 1) + 1)) -' 1) -' 1) + 1 & (((h . ((k + 1) + 1)) -' 1) -' 1) + 1 < h . ((k + 1) + 1) implies (accum g) . ((((h . ((k + 1) + 1)) -' 1) -' 1) + 1) = (accum F) . (k + 1) ) ;
now :: thesis: ( ( 1 <= k & (accum g) . (h . ((k + 1) + 1)) = (accum F) . ((k + 1) + 1) ) or ( k < 1 & (accum g) . (h . ((k + 1) + 1)) = (accum F) . ((k + 1) + 1) ) )
per cases ( 1 <= k or k < 1 ) ;
case A108: 1 <= k ; :: thesis: (accum g) . (h . ((k + 1) + 1)) = (accum F) . ((k + 1) + 1)
k < k + 1 by XREAL_1:29;
then A109: k < len h by A36, A22, A83, XXREAL_0:2;
then k <= h . k by A1, A26, Th7;
then A110: 1 <= h . k by A108, XXREAL_0:2;
A111: 1 + (h . (k + 1)) <= h . ((k + 1) + 1) by A89, NAT_1:13;
then A112: ((h . (k + 1)) + 1) - 1 <= (h . ((k + 1) + 1)) - 1 by XREAL_1:9;
h . k < h . (k + 1) by A1, A108, A109;
then 1 < h . (k + 1) by A110, XXREAL_0:2;
then 1 + 1 < (h . (k + 1)) + 1 by XREAL_1:6;
then 1 + 1 < h . ((k + 1) + 1) by A111, XXREAL_0:2;
then A113: (1 + 1) - 1 < (h . ((k + 1) + 1)) - 1 by XREAL_1:9;
then A114: (h . ((k + 1) + 1)) -' 1 = (h . ((k + 1) + 1)) - 1 by XREAL_0:def 2;
then A115: ((h . ((k + 1) + 1)) -' 1) -' 1 = ((h . ((k + 1) + 1)) - 1) - 1 by A113, XREAL_1:233;
A116: g /. (h . ((k + 1) + 1)) = g . (h . ((k + 1) + 1)) by A81, A88, FINSEQ_4:15;
A117: F . ((k + 1) + 1) = g . (h . ((k + 1) + 1)) by A3, A36, A21, A79, FUNCT_1:13;
A118: k + 1 <= len (accum F) by A78, A82, XXREAL_0:2;
h . ((k + 1) + 1) < (h . ((k + 1) + 1)) + 1 by XREAL_1:29;
then A119: (h . ((k + 1) + 1)) - 1 < ((h . ((k + 1) + 1)) + 1) - 1 by XREAL_1:9;
then A120: (h . ((k + 1) + 1)) -' 1 < len g by A88, A114, XXREAL_0:2;
then A121: (accum g) /. ((h . ((k + 1) + 1)) -' 1) = (accum g) . ((h . ((k + 1) + 1)) -' 1) by A32, A113, A114, FINSEQ_4:15;
(accum F) . ((k + 1) + 1) = ((accum F) /. (k + 1)) + (F /. ((k + 1) + 1)) by A36, A38, A83, NAT_1:11
.= ((accum g) /. ((h . ((k + 1) + 1)) -' 1)) + (F /. ((k + 1) + 1)) by A107, A114, A115, A112, A119, A121, A118, FINSEQ_4:15, NAT_1:11
.= ((accum g) /. ((h . ((k + 1) + 1)) -' 1)) + (g /. (h . ((k + 1) + 1))) by A36, A77, A78, A117, A116, FINSEQ_4:15
.= (accum g) . (((h . ((k + 1) + 1)) -' 1) + 1) by Def10, A113, A114, A120 ;
hence (accum g) . (h . ((k + 1) + 1)) = (accum F) . ((k + 1) + 1) by A114; :: thesis: verum
end;
case k < 1 ; :: thesis: (accum g) . (h . ((k + 1) + 1)) = (accum F) . ((k + 1) + 1)
then A122: k = 0 by NAT_1:14;
then 1 < len h by A36, A22, A78, NAT_1:13;
then A123: h . 1 < h . (1 + 1) by A1;
then A124: (h . (1 + 1)) -' 1 = (h . (1 + 1)) - 1 by A31, XREAL_1:233, XXREAL_0:2;
then A125: ((h . ((k + 1) + 1)) -' 1) + 1 = h . ((k + 1) + 1) by A122;
A126: F /. 1 = F . 1 by A19, A22, FINSEQ_4:15;
k + 1 < len F by A36, A78, NAT_1:13;
then A127: (accum F) . ((k + 1) + 1) = ((accum F) /. (k + 1)) + (F /. ((k + 1) + 1)) by A38, NAT_1:11
.= (F /. 1) + (F /. (1 + 1)) by A36, A37, A19, A22, A122, A126, FINSEQ_4:15 ;
A128: F /. (1 + 1) = F . (1 + 1) by A36, A78, A122, FINSEQ_4:15;
(h . 1) + 1 <= h . (1 + 1) by A123, NAT_1:13;
then ((h . 1) + 1) - 1 <= (h . (1 + 1)) - 1 by XREAL_1:9;
then A129: h . 1 <= (h . (1 + 1)) -' 1 by A26, A123, XREAL_1:233, XXREAL_0:2;
h . (1 + 1) < (h . (1 + 1)) + 1 by XREAL_1:29;
then A130: (h . (1 + 1)) - 1 < ((h . (1 + 1)) + 1) - 1 by XREAL_1:9;
then A131: (h . (1 + 1)) -' 1 < h . (1 + 1) by A26, A123, XREAL_1:233, XXREAL_0:2;
A132: 1 < h . (1 + 1) by A26, A123, XXREAL_0:2;
then 1 + 1 <= h . (1 + 1) by NAT_1:13;
then A133: (1 + 1) - 1 <= (h . (1 + 1)) - 1 by XREAL_1:9;
then ((h . (1 + 1)) -' 1) -' 1 = ((h . (1 + 1)) -' 1) - 1 by A124, XREAL_1:233;
then A134: (((h . (1 + 1)) -' 1) -' 1) + 1 = (h . (1 + 1)) -' 1 ;
1 + 1 in Seg (len h) by A36, A22, A78, A122, FINSEQ_1:1;
then 1 + 1 in dom h by FINSEQ_1:def 3;
then h . (1 + 1) in rng h by FUNCT_1:def 3;
then h . (1 + 1) in dom g by A2;
then A135: h . (1 + 1) in Seg (len g) by FINSEQ_1:def 3;
then h . (1 + 1) <= len g by FINSEQ_1:1;
then A136: g /. (h . ((k + 1) + 1)) = g . (h . (1 + 1)) by A122, A132, FINSEQ_4:15
.= F . (1 + 1) by A3, A36, A21, A79, A122, FUNCT_1:13 ;
h . (1 + 1) <= len g by A135, FINSEQ_1:1;
then (h . (1 + 1)) -' 1 < len (accum g) by A32, A124, A130, XXREAL_0:2;
then A137: (accum g) /. ((h . ((k + 1) + 1)) -' 1) = (accum g) . ((h . (1 + 1)) -' 1) by A122, A124, A133, FINSEQ_4:15
.= F . 1 by A37, A106, A122, A134, A131, A129 ;
h . (1 + 1) <= len g by A135, FINSEQ_1:1;
then A138: (h . ((k + 1) + 1)) -' 1 < len g by A122, A125, NAT_1:13;
1 <= (h . ((k + 1) + 1)) -' 1 by A122, A132, A125, NAT_1:13;
then (accum g) . (((h . ((k + 1) + 1)) -' 1) + 1) = ((accum g) /. ((h . ((k + 1) + 1)) -' 1)) + (g /. (h . ((k + 1) + 1))) by Def10, A122, A124, A138
.= (F /. 1) + (F /. (1 + 1)) by A19, A22, A128, A137, A136, FINSEQ_4:15 ;
hence (accum g) . (h . ((k + 1) + 1)) = (accum F) . ((k + 1) + 1) by A122, A124, A127; :: thesis: verum
end;
end;
end;
hence (accum g) . (h . ((k + 1) + 1)) = (accum F) . ((k + 1) + 1) ; :: thesis: verum
end;
hence S2[k + 1] ; :: thesis: verum
end;
defpred S3[ Nat] means ( h . (len h) <= $1 + 1 & $1 + 1 <= len g implies (accum g) . ($1 + 1) = (accum F) . (len (accum F)) );
A139: S2[ 0 ] by A64;
A140: for k being Nat holds S2[k] from NAT_1:sch 2(A139, A75);
A141: for k being Nat st S3[k] holds
S3[k + 1]
proof
let k be Nat; :: thesis: ( S3[k] implies S3[k + 1] )
assume A142: S3[k] ; :: thesis: S3[k + 1]
( h . (len h) <= (k + 1) + 1 & (k + 1) + 1 <= len g implies (accum g) . ((k + 1) + 1) = (accum F) . (len (accum F)) )
proof
assume that
A143: h . (len h) <= (k + 1) + 1 and
A144: (k + 1) + 1 <= len g ; :: thesis: (accum g) . ((k + 1) + 1) = (accum F) . (len (accum F))
per cases ( h . (len h) < (k + 1) + 1 or h . (len h) = (k + 1) + 1 ) by A143, XXREAL_0:1;
suppose A145: h . (len h) < (k + 1) + 1 ; :: thesis: (accum g) . ((k + 1) + 1) = (accum F) . (len (accum F))
A146: now :: thesis: not (k + 1) + 1 in rng h
assume (k + 1) + 1 in rng h ; :: thesis: contradiction
then consider x being object such that
A147: x in dom h and
A148: h . x = (k + 1) + 1 by FUNCT_1:def 3;
reconsider nx = x as Element of NAT by A147;
A149: x in Seg (len h) by A147, FINSEQ_1:def 3;
then A150: nx <= len h by FINSEQ_1:1;
1 <= nx by A149, FINSEQ_1:1;
hence contradiction by A1, A145, A148, A150, Th6; :: thesis: verum
end;
1 <= (k + 1) + 1 by NAT_1:11;
then (k + 1) + 1 in Seg (len g) by A144, FINSEQ_1:1;
then A151: (k + 1) + 1 in dom g by FINSEQ_1:def 3;
k + 1 < (k + 1) + 1 by XREAL_1:29;
then A152: k + 1 < len g by A144, XXREAL_0:2;
then A153: (accum g) . ((k + 1) + 1) = ((accum g) /. (k + 1)) + (g /. ((k + 1) + 1)) by A34, NAT_1:11;
1 <= k + 1 by NAT_1:11;
then A154: (accum g) /. (k + 1) = (accum F) . (len (accum F)) by A32, A142, A145, A152, FINSEQ_4:15, NAT_1:13;
1 < (k + 1) + 1 by XREAL_1:29;
then g /. ((k + 1) + 1) = g . ((k + 1) + 1) by A144, FINSEQ_4:15
.= 0* n by A4, A146, A151 ;
hence (accum g) . ((k + 1) + 1) = (accum F) . (len (accum F)) by A154, A153, EUCLID_4:1; :: thesis: verum
end;
suppose A155: h . (len h) = (k + 1) + 1 ; :: thesis: (accum g) . ((k + 1) + 1) = (accum F) . (len (accum F))
A156: (len h) -' 1 = (len h) - 1 by A19, XREAL_1:233;
( 1 <= ((len h) -' 1) + 1 & ((len h) -' 1) + 1 <= len (accum F) implies (accum g) . (h . (((len h) -' 1) + 1)) = (accum F) . (((len h) -' 1) + 1) ) by A140;
hence (accum g) . ((k + 1) + 1) = (accum F) . (len (accum F)) by A36, A18, A21, A155, A156, FINSEQ_1:1, FINSEQ_1:def 3; :: thesis: verum
end;
end;
end;
hence S3[k + 1] ; :: thesis: verum
end;
A157: 1 <= h . (len h) by A20, FINSEQ_1:1;
( h . (len h) <= 1 & 1 <= len g implies (accum g) . (0 + 1) = (accum F) . (len (accum F)) )
proof
assume that
A158: h . (len h) <= 1 and
1 <= len g ; :: thesis: (accum g) . (0 + 1) = (accum F) . (len (accum F))
h . (len h) = 1 by A157, A158, XXREAL_0:1;
then len h <= 1 by A1, A26, Th7;
then A159: len h = 1 by A19, XXREAL_0:1;
(accum F) . 1 = g . (h . 1) by A3, A5, A37, A17, FUNCT_1:13
.= g . 1 by A157, A158, A159, XXREAL_0:1 ;
hence (accum g) . (0 + 1) = (accum F) . (len (accum F)) by A6, A36, A33, A159, FINSEQ_1:def 3; :: thesis: verum
end;
then A160: S3[ 0 ] ;
for k being Nat holds S3[k] from NAT_1:sch 2(A160, A141);
hence Sum g = Sum F by A36, A39, A35, A29, A30; :: thesis: verum
end;
suppose A161: len F <= 0 ; :: thesis: Sum g = Sum F
then A162: Sum F = 0* n by Def11;
A163: dom g = Seg (len g) by FINSEQ_1:def 3;
Seg (len F) = {} by A161;
then dom F = {} by FINSEQ_1:def 3;
then A164: rng h = {} by A3, A5, RELAT_1:42;
A165: now :: thesis: for z being object st z in dom g holds
g . z = ((len g) |-> (0* n)) . z
let z be object ; :: thesis: ( z in dom g implies g . z = ((len g) |-> (0* n)) . z )
assume A166: z in dom g ; :: thesis: g . z = ((len g) |-> (0* n)) . z
hence g . z = 0* n by A4, A164
.= ((len g) |-> (0* n)) . z by A163, A166, FINSEQ_2:57 ;
:: thesis: verum
end;
Seg (len g) = dom ((len g) |-> (0* n)) by FUNCOP_1:13;
then g = (len g) |-> (0* n) by A163, A165, FUNCT_1:2;
hence Sum g = Sum F by A162, Th21; :: thesis: verum
end;
end;