defpred S1[ Nat] means for f, h being natural-valued FinSequence st len f = $1 & ( for i being Nat holds card (Coim (h,i)) = f . i ) holds
Sum h = (((id (dom f)) (#) f),1) +... ;
A1: S1[ 0 ]
proof
let f, h be natural-valued FinSequence; :: thesis: ( len f = 0 & ( for i being Nat holds card (Coim (h,i)) = f . i ) implies Sum h = (((id (dom f)) (#) f),1) +... )
assume that
A2: len f = 0 and
A3: for i being Nat holds card (Coim (h,i)) = f . i ; :: thesis: Sum h = (((id (dom f)) (#) f),1) +...
set L = (len h) |-> 0;
now :: thesis: for i being Nat st 1 <= i & i <= len h holds
h . i = ((len h) |-> 0) . i
let i be Nat; :: thesis: ( 1 <= i & i <= len h implies h . i = ((len h) |-> 0) . i )
assume A4: ( 1 <= i & i <= len h ) ; :: thesis: h . i = ((len h) |-> 0) . i
A5: i in dom h by A4, FINSEQ_3:25;
f = {} by A2;
then f . (h . i) = 0 ;
then card (Coim (h,(h . i))) = 0 by A3;
then Coim (h,(h . i)) = {} ;
then h " {(h . i)} = {} by RELAT_1:def 17;
then not h . i in rng h by FUNCT_1:72;
hence h . i = ((len h) |-> 0) . i by A5, FUNCT_1:def 3; :: thesis: verum
end;
then A6: h = (len h) |-> 0 by CARD_1:def 7;
A7: f = {} by A2;
then reconsider E = (id (dom f)) (#) f as complex-valued FinSequence ;
(((id (dom f)) (#) f),1) +... = (E . 1) + ((E,(1 + 1)) +...) by FLEXARY1:20
.= Sum E by FLEXARY1:22
.= 0 by A7, RVSUM_1:72 ;
hence Sum h = (((id (dom f)) (#) f),1) +... by A6, RVSUM_1:81; :: thesis: verum
end;
A8: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A9: S1[i] ; :: thesis: S1[i + 1]
set i1 = i + 1;
let f, h be natural-valued FinSequence; :: thesis: ( len f = i + 1 & ( for i being Nat holds card (Coim (h,i)) = f . i ) implies Sum h = (((id (dom f)) (#) f),1) +... )
assume that
A10: len f = i + 1 and
A11: for i being Nat holds card (Coim (h,i)) = f . i ; :: thesis: Sum h = (((id (dom f)) (#) f),1) +...
A12: id (dom f) = idseq (i + 1) by FINSEQ_1:def 3, A10;
set fi = f | i;
A13: f = (f | i) ^ <*(f . (i + 1))*> by A10, FINSEQ_3:55;
A14: i < i + 1 by NAT_1:13;
then A15: len (f | i) = i by A10, FINSEQ_1:59;
then A16: id (dom (f | i)) = idseq i by FINSEQ_1:def 3;
A17: idseq (i + 1) = (idseq i) ^ <*(i + 1)*> by FINSEQ_2:51;
len (f | i) = len (idseq i) by CARD_1:def 7, A15;
then A18: (id (dom f)) (#) f = ((idseq i) (#) (f | i)) ^ (<*(i + 1)*> (#) <*(f . (i + 1))*>) by Th8, A12, A13, A17;
A19: (Seg 1) /\ (Seg 1) = Seg 1 ;
( dom <*(i + 1)*> = Seg 1 & dom <*(f . (i + 1))*> = Seg 1 ) by FINSEQ_1:38;
then dom (<*(i + 1)*> (#) <*(f . (i + 1))*>) = Seg 1 by VALUED_1:def 4, A19;
then A20: len (<*(i + 1)*> (#) <*(f . (i + 1))*>) = 1 by FINSEQ_1:def 3;
( <*(i + 1)*> . 1 = i + 1 & <*(f . (i + 1))*> . 1 = f . (i + 1) ) by FINSEQ_1:40;
then (<*(i + 1)*> (#) <*(f . (i + 1))*>) . 1 = (i + 1) * (f . (i + 1)) by VALUED_1:5;
then A21: <*(i + 1)*> (#) <*(f . (i + 1))*> = <*((i + 1) * (f . (i + 1)))*> by A20, FINSEQ_1:40;
A22: (((id (dom f)) (#) f),1) +... = Sum ((idseq (i + 1)) (#) f) by A12, FLEXARY1:21;
per cases ( f . (i + 1) = 0 or f . (i + 1) <> 0 ) ;
suppose A23: f . (i + 1) = 0 ; :: thesis: Sum h = (((id (dom f)) (#) f),1) +...
then A24: (((id (dom f)) (#) f),1) +... = (Sum ((idseq i) (#) (f | i))) + 0 by A21, A12, A18, A22, RVSUM_1:74;
for j being Nat holds card (Coim (h,j)) = (f | i) . j
proof
let j be Nat; :: thesis: card (Coim (h,j)) = (f | i) . j
per cases ( j in dom (f | i) or j = i + 1 or ( j <> i + 1 & not j in dom (f | i) ) ) ;
suppose j in dom (f | i) ; :: thesis: card (Coim (h,j)) = (f | i) . j
then ( (f | i) . j = f . j & f . j = card (Coim (h,j)) ) by A11, FUNCT_1:47;
hence card (Coim (h,j)) = (f | i) . j ; :: thesis: verum
end;
suppose A25: j = i + 1 ; :: thesis: card (Coim (h,j)) = (f | i) . j
then not j in dom (f | i) by A14, A15, FINSEQ_3:25;
then ( (f | i) . j = 0 & f . j = card (Coim (h,j)) ) by A11, FUNCT_1:def 2;
hence card (Coim (h,j)) = (f | i) . j by A23, A25; :: thesis: verum
end;
suppose A26: ( j <> i + 1 & not j in dom (f | i) ) ; :: thesis: card (Coim (h,j)) = (f | i) . j
then A27: (f | i) . j = 0 by FUNCT_1:def 2;
( j < 1 or j > i ) by A26, A15, FINSEQ_3:25;
then ( j < 1 or j >= i + 1 ) by NAT_1:13;
then ( j < 1 or j > i + 1 ) by A26, XXREAL_0:1;
then not j in dom f by A10, FINSEQ_3:25;
then f . j = 0 by FUNCT_1:def 2;
hence card (Coim (h,j)) = (f | i) . j by A11, A27; :: thesis: verum
end;
end;
end;
then Sum h = (((idseq i) (#) (f | i)),1) +... by A9, A16, A15
.= Sum ((idseq i) (#) (f | i)) by FLEXARY1:21 ;
hence Sum h = (((id (dom f)) (#) f),1) +... by A24; :: thesis: verum
end;
suppose f . (i + 1) <> 0 ; :: thesis: Sum h = (((id (dom f)) (#) f),1) +...
then card (Coim (h,(i + 1))) <> 0 by A11;
then Coim (h,(i + 1)) <> {} ;
then consider xx being object such that
A28: xx in Coim (h,(i + 1)) by XBOOLE_0:def 1;
A29: ( xx in Coim (h,(i + 1)) & Coim (h,(i + 1)) = h " {(i + 1)} ) by A28, RELAT_1:def 17;
then reconsider D = dom h as non empty set by FUNCT_1:def 7;
A30: rng h c= REAL ;
then reconsider H = h as Function of D,REAL by FUNCT_2:2;
reconsider h1 = H as FinSequence of REAL by A30, FINSEQ_1:def 4;
set X = h " {(i + 1)};
set Y = D \ (h " {(i + 1)});
dom (H | ((D \ (h " {(i + 1)})) \/ (h " {(i + 1)}))) is finite ;
then A31: FinS (H,((D \ (h " {(i + 1)})) \/ (h " {(i + 1)}))),(FinS (H,(D \ (h " {(i + 1)})))) ^ (FinS (H,(h " {(i + 1)}))) are_fiberwise_equipotent by RFUNCT_3:76, XBOOLE_1:79;
A32: D = (h " {(i + 1)}) \/ (D \ (h " {(i + 1)})) by RELAT_1:132, XBOOLE_1:45;
H | D = H ;
then H, FinS (H,((h " {(i + 1)}) \/ (D \ (h " {(i + 1)})))) are_fiberwise_equipotent by A32, RFUNCT_3:def 13;
then A33: Sum h1 = Sum ((FinS (H,(D \ (h " {(i + 1)})))) ^ (FinS (H,(h " {(i + 1)})))) by A31, CLASSES1:76, RFINSEQ:9
.= (Sum (FinS (H,(D \ (h " {(i + 1)}))))) + (Sum (FinS (H,(h " {(i + 1)})))) by RVSUM_1:75 ;
A34: ( dom (H | (h " {(i + 1)})) = h " {(i + 1)} & dom (H | (D \ (h " {(i + 1)}))) = D \ (h " {(i + 1)}) ) by RELAT_1:132, RELAT_1:62;
rng (H | (h " {(i + 1)})) c= {(i + 1)}
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (H | (h " {(i + 1)})) or y in {(i + 1)} )
assume y in rng (H | (h " {(i + 1)})) ; :: thesis: y in {(i + 1)}
then consider x being object such that
A35: ( x in h " {(i + 1)} & (H | (h " {(i + 1)})) . x = y ) by A34, FUNCT_1:def 3;
(H | (h " {(i + 1)})) . x = H . x by A35, FUNCT_1:49;
hence y in {(i + 1)} by A35, FUNCT_1:def 7; :: thesis: verum
end;
then FinS (H,(h " {(i + 1)})) = (card (h " {(i + 1)})) |-> (i + 1) by A29, A34, ZFMISC_1:33, RFUNCT_3:75;
then A36: FinS (H,(h " {(i + 1)})) = (f . (i + 1)) |-> (i + 1) by A29, A11;
A37: H | (D \ (h " {(i + 1)})), FinS (H,(D \ (h " {(i + 1)}))) are_fiberwise_equipotent by A34, RFUNCT_3:def 13;
then rng (H | (D \ (h " {(i + 1)}))) = rng (FinS (H,(D \ (h " {(i + 1)})))) by CLASSES1:75;
then rng (FinS (H,(D \ (h " {(i + 1)})))) c= NAT by VALUED_0:def 6;
then reconsider F = FinS (H,(D \ (h " {(i + 1)}))) as natural-valued FinSequence by VALUED_0:def 6;
for j being Nat holds card (Coim (F,j)) = (f | i) . j
proof
let j be Nat; :: thesis: card (Coim (F,j)) = (f | i) . j
set hY = h | (D \ (h " {(i + 1)}));
A38: card (Coim (F,j)) = card (Coim ((h | (D \ (h " {(i + 1)}))),j)) by A37, CLASSES1:def 10;
A39: ( (h | (D \ (h " {(i + 1)}))) " {j} = Coim ((h | (D \ (h " {(i + 1)}))),j) & h " {j} = Coim (h,j) ) by RELAT_1:def 17;
A40: (h | (D \ (h " {(i + 1)}))) " {j} = (D \ (h " {(i + 1)})) /\ (h " {j}) by FUNCT_1:70
.= ((h " {j}) /\ D) \ (h " {(i + 1)}) by XBOOLE_1:49
.= (h " {j}) \ (h " {(i + 1)}) by RELAT_1:132, XBOOLE_1:28
.= h " ({j} \ {(i + 1)}) by FUNCT_1:69 ;
A41: card (Coim (h,j)) = f . j by A11;
per cases ( j in dom (f | i) or j = i + 1 or ( not j in dom (f | i) & j <> i + 1 ) ) ;
suppose A42: j in dom (f | i) ; :: thesis: card (Coim (F,j)) = (f | i) . j
then j <> i + 1 by A15, FINSEQ_3:25, A14;
then card (Coim (F,j)) = card (Coim (h,j)) by ZFMISC_1:14, A38, A39, A40;
hence card (Coim (F,j)) = (f | i) . j by A41, A42, FUNCT_1:47; :: thesis: verum
end;
suppose A43: j = i + 1 ; :: thesis: card (Coim (F,j)) = (f | i) . j
then A44: not j in dom (f | i) by A14, A15, FINSEQ_3:25;
card (Coim (F,j)) = card (h " {}) by A43, A38, A39, A40;
hence card (Coim (F,j)) = (f | i) . j by A44, FUNCT_1:def 2; :: thesis: verum
end;
suppose A45: ( not j in dom (f | i) & j <> i + 1 ) ; :: thesis: card (Coim (F,j)) = (f | i) . j
then A46: (f | i) . j = 0 by FUNCT_1:def 2;
( j < 1 or j > i ) by A45, A15, FINSEQ_3:25;
then ( j < 1 or j >= i + 1 ) by NAT_1:13;
then ( j < 1 or j > i + 1 ) by A45, XXREAL_0:1;
then A47: not j in dom f by A10, FINSEQ_3:25;
card (Coim (F,j)) = card (Coim (h,j)) by A45, ZFMISC_1:14, A38, A39, A40;
hence card (Coim (F,j)) = (f | i) . j by A46, A47, FUNCT_1:def 2, A41; :: thesis: verum
end;
end;
end;
then A48: Sum F = (((idseq i) (#) (f | i)),1) +... by A9, A15, A16
.= Sum ((idseq i) (#) (f | i)) by FLEXARY1:21 ;
(((id (dom f)) (#) f),1) +... = (Sum ((idseq i) (#) (f | i))) + ((i + 1) * (f . (i + 1))) by A21, A12, A18, A22, RVSUM_1:74;
hence Sum h = (((id (dom f)) (#) f),1) +... by A33, A48, A36, RVSUM_1:80; :: thesis: verum
end;
end;
end;
A49: for i being Nat holds S1[i] from NAT_1:sch 2(A1, A8);
 let f, h be natural-valued FinSequence; :: thesis: ( ( for i being Nat holds card (Coim (h,i)) = f . i ) implies Sum h = ((1 * (f . 1)) + (2 * (f . 2))) + ((((id (dom f)) (#) f),3) +...) )
assume A50: for i being Nat holds card (Coim (h,i)) = f . i ; :: thesis: Sum h = ((1 * (f . 1)) + (2 * (f . 2))) + ((((id (dom f)) (#) f),3) +...)
set I = (idseq (len f)) (#) f;
A51: id (dom f) = idseq (len f) by FINSEQ_1:def 3;
then A52: ((idseq (len f)) (#) f) . 1 = 1 * (f . 1) by Lm2;
A53: ((idseq (len f)) (#) f) . 2 = 2 * (f . 2) by Lm2, A51;
Sum h = (((idseq (len f)) (#) f),1) +... by A49, A51, A50
.= (((idseq (len f)) (#) f) . 1) + ((((idseq (len f)) (#) f),(1 + 1)) +...) by FLEXARY1:20
.= (((idseq (len f)) (#) f) . 1) + ((((idseq (len f)) (#) f) . 2) + ((((idseq (len f)) (#) f),(2 + 1)) +...)) by FLEXARY1:20 ;
hence Sum h = ((1 * (f . 1)) + (2 * (f . 2))) + ((((id (dom f)) (#) f),3) +...) by A52, A53, A51; :: thesis: verum