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