let u be INT -valued FinSequence; :: thesis: for m being CR_Sequence st len m = len u holds
for c being CR_coefficients of m
for i being Nat st i in dom m holds
Sum (u (#) c),u . i are_congruent_mod m . i
let m be CR_Sequence; :: thesis: ( len m = len u implies for c being CR_coefficients of m
for i being Nat st i in dom m holds
Sum (u (#) c),u . i are_congruent_mod m . i )
assume A1: len m = len u ; :: thesis: for c being CR_coefficients of m
for i being Nat st i in dom m holds
Sum (u (#) c),u . i are_congruent_mod m . i
let c be CR_coefficients of m; :: thesis: for i being Nat st i in dom m holds
Sum (u (#) c),u . i are_congruent_mod m . i
let i be Nat; :: thesis: ( i in dom m implies Sum (u (#) c),u . i are_congruent_mod m . i )
defpred S₁[ Nat] means for v, cc being INT -valued FinSequence st v = u | $1 & cc = c | $1 & not ( $1 < i & Sum (v (#) cc), 0 are_congruent_mod m . i ) holds
( $1 >= i & Sum (v (#) cc),u . i are_congruent_mod m . i );
assume A2: i in dom m ; :: thesis: Sum (u (#) c),u . i are_congruent_mod m . i
A3: len m = len c by Def4;
then A4: dom m = Seg (len c) by FINSEQ_1:def 3
.= dom c by FINSEQ_1:def 3 ;

A5: now :: thesis: for k being Element of NAT st 0 <= k & k < len u & S₁[k] holds
S₁[k + 1]

let k be Element of NAT ; :: thesis: ( 0 <= k & k < len u & S₁[k] implies S₁[k + 1] )
assume that
0 <= k and
A6: k < len u and
A7: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: for v, cc being INT -valued FinSequence st v = u | (k + 1) & cc = c | (k + 1) & not ( k + 1 < i & Sum (v (#) cc), 0 are_congruent_mod m . i ) holds
( k + 1 >= i & Sum (v (#) cc),u . i are_congruent_mod m . i )

set v9 = u | k;
set cc9 = c | k;
let v, cc be INT -valued FinSequence; :: thesis: ( v = u | (k + 1) & cc = c | (k + 1) & not ( k + 1 < i & Sum (v (#) cc), 0 are_congruent_mod m . i ) implies ( k + 1 >= i & Sum (v (#) cc),u . i are_congruent_mod m . i ) )
A8: 0 + 1 <= k + 1 by XREAL_1:6;
reconsider a = v (#) cc, b = (u | k) (#) (c | k) as FinSequence of REAL by FINSEQ_1:102;
assume that
A9: v = u | (k + 1) and
A10: cc = c | (k + 1) ; :: thesis: ( ( k + 1 < i & Sum (v (#) cc), 0 are_congruent_mod m . i ) or ( k + 1 >= i & Sum (v (#) cc),u . i are_congruent_mod m . i ) )
k + 1 <= len u by A6, NAT_1:13;
then len v = k + 1 by A9, FINSEQ_1:59;
then k + 1 in Seg (len v) by A8;
then k + 1 in dom v by FINSEQ_1:def 3;
then A11: v . (k + 1) = u . (k + 1) by A9, FUNCT_1:47;
A12: k + 1 <= len c by A1, A3, A6, NAT_1:13;
then k + 1 in Seg (len c) by A8;
then A13: k + 1 in dom c by FINSEQ_1:def 3;
reconsider r = (v . (k + 1)) * (cc . (k + 1)) as Element of REAL by XREAL_0:def 1;
reconsider s = <*r*> as FinSequence of REAL ;
A14: len u = len c by A1, Def4;
len cc = k + 1 by A10, A12, FINSEQ_1:59;
then k + 1 in Seg (len cc) by A8;
then k + 1 in dom cc by FINSEQ_1:def 3;
then A15: cc . (k + 1) = c . (k + 1) by A10, FUNCT_1:47;
A16: k + 1 <= len u by A6, NAT_1:13;
A17: ((u (#) c) | k) ^ <*((v . (k + 1)) * (cc . (k + 1)))*> = (u (#) c) | (k + 1)

proof

set p = ((u (#) c) | k) ^ <*((v . (k + 1)) * (cc . (k + 1)))*>;
set q = (u (#) c) | (k + 1);
A18: k + 1 <= len (u (#) c) by A1, A3, A16, Lm4;
then A19: k <= len (u (#) c) by NAT_1:13;
A20: len (((u (#) c) | k) ^ <*((v . (k + 1)) * (cc . (k + 1)))*>) = (len ((u (#) c) | k)) + 1 by FINSEQ_2:16
.= k + 1 by A19, FINSEQ_1:59 ;
A21: k + 1 = len ((u (#) c) | (k + 1)) by A18, FINSEQ_1:59;

now :: thesis: for j being Nat st 1 <= j & j <= len (((u (#) c) | k) ^ <*((v . (k + 1)) * (cc . (k + 1)))*>) holds
(((u (#) c) | k) ^ <*((v . (k + 1)) * (cc . (k + 1)))*>) . j = ((u (#) c) | (k + 1)) . j

let j be Nat; :: thesis: ( 1 <= j & j <= len (((u (#) c) | k) ^ <*((v . (k + 1)) * (cc . (k + 1)))*>) implies (((u (#) c) | k) ^ <*((v . (k + 1)) * (cc . (k + 1)))*>) . b₁ = ((u (#) c) | (k + 1)) . b₁ )
assume that
A22: 1 <= j and
A23: j <= len (((u (#) c) | k) ^ <*((v . (k + 1)) * (cc . (k + 1)))*>) ; :: thesis: (((u (#) c) | k) ^ <*((v . (k + 1)) * (cc . (k + 1)))*>) . b₁ = ((u (#) c) | (k + 1)) . b₁

per cases ( j in dom ((u (#) c) | k) or not j in dom ((u (#) c) | k) ) ;

suppose A24: j in dom ((u (#) c) | k) ; :: thesis: (((u (#) c) | k) ^ <*((v . (k + 1)) * (cc . (k + 1)))*>) . b₁ = ((u (#) c) | (k + 1)) . b₁

j in Seg (k + 1) by A20, A22, A23;
then A25: j in dom ((u (#) c) | (k + 1)) by A21, FINSEQ_1:def 3;
thus (((u (#) c) | k) ^ <*((v . (k + 1)) * (cc . (k + 1)))*>) . j = ((u (#) c) | k) . j by A24, FINSEQ_1:def 7
.= (u (#) c) . j by A24, FUNCT_1:47
.= ((u (#) c) | (k + 1)) . j by A25, FUNCT_1:47 ; :: thesis: verum

end;

suppose A26: not j in dom ((u (#) c) | k) ; :: thesis: (((u (#) c) | k) ^ <*((v . (k + 1)) * (cc . (k + 1)))*>) . b₁ = ((u (#) c) | (k + 1)) . b₁

k <= len (u (#) c) by A6, A14, Lm4;
then A27: len ((u (#) c) | k) = k by FINSEQ_1:59;
then dom ((u (#) c) | k) = Seg k by FINSEQ_1:def 3;
then j > k by A22, A26;
then A28: j >= k + 1 by NAT_1:13;
then A29: j = k + 1 by A20, A23, XXREAL_0:1;
dom <*((v . (k + 1)) * (cc . (k + 1)))*> = {1} by FINSEQ_1:2, FINSEQ_1:38;
then 1 in dom <*((v . (k + 1)) * (cc . (k + 1)))*> by TARSKI:def 1;
then A30: (((u (#) c) | k) ^ <*((v . (k + 1)) * (cc . (k + 1)))*>) . (k + 1) = <*((v . (k + 1)) * (cc . (k + 1)))*> . 1 by A27, FINSEQ_1:def 7
.= (v . (k + 1)) * (cc . (k + 1)) ;
k + 1 <= len (u (#) c) by A12, A14, Lm4;
then j in Seg (len (u (#) c)) by A8, A29;
then A31: j in dom (u (#) c) by FINSEQ_1:def 3;
j in Seg (k + 1) by A20, A22, A23;
then j in dom ((u (#) c) | (k + 1)) by A21, FINSEQ_1:def 3;
then ((u (#) c) | (k + 1)) . j = (u (#) c) . j by FUNCT_1:47
.= (v . (k + 1)) * (cc . (k + 1)) by A15, A11, A29, A31, VALUED_1:def 4 ;
hence (((u (#) c) | k) ^ <*((v . (k + 1)) * (cc . (k + 1)))*>) . j = ((u (#) c) | (k + 1)) . j by A20, A23, A28, A30, XXREAL_0:1; :: thesis: verum

end;

end;

end;

hence ((u (#) c) | k) ^ <*((v . (k + 1)) * (cc . (k + 1)))*> = (u (#) c) | (k + 1) by A20, A21; :: thesis: verum

end;

(u | k) (#) (c | k) = (u (#) c) | k by A6, A14, Th4;
then a = b ^ s by A9, A10, A16, A14, A17, Th4;
then A32: Sum (v (#) cc) = (Sum b) + (Sum s) by RVSUM_1:75
.= (Sum ((u | k) (#) (c | k))) + ((v . (k + 1)) * (cc . (k + 1))) by RVSUM_1:73 ;
A33: k < k + 1 by NAT_1:13;

now :: thesis: ( ( k + 1 < i & Sum (v (#) cc), 0 are_congruent_mod m . i ) or ( k + 1 = i & Sum (v (#) cc),0 + (u . i) are_congruent_mod m . i ) or ( k + 1 > i & Sum (v (#) cc),(u . i) + 0 are_congruent_mod m . i ) )

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

case A34: k + 1 < i ; :: thesis: Sum (v (#) cc), 0 are_congruent_mod m . i

then k < i by NAT_1:13;
then A35: Sum ((u | k) (#) (c | k)), 0 are_congruent_mod m . i by A7;
A36: v . (k + 1),v . (k + 1) are_congruent_mod m . i by INT_1:11;
cc . (k + 1), 0 are_congruent_mod m . i by A2, A4, A13, A15, A34, Th27;
then (v . (k + 1)) * (cc . (k + 1)),(v . (k + 1)) * 0 are_congruent_mod m . i by A36, INT_1:18;
then Sum (v (#) cc),0 + ((v . (k + 1)) * 0) are_congruent_mod m . i by A32, A35, INT_1:16;
hence Sum (v (#) cc), 0 are_congruent_mod m . i ; :: thesis: verum

end;

case A37: k + 1 = i ; :: thesis: Sum (v (#) cc),0 + (u . i) are_congruent_mod m . i

A38: v . (k + 1),v . (k + 1) are_congruent_mod m . i by INT_1:11;
cc . (k + 1),1 are_congruent_mod m . i by A13, A15, A37, Th26;
then A39: (v . (k + 1)) * (cc . (k + 1)),(u . (k + 1)) * 1 are_congruent_mod m . i by A11, A38, INT_1:18;
Sum ((u | k) (#) (c | k)), 0 are_congruent_mod m . i by A7, A33, A37;
hence Sum (v (#) cc),0 + (u . i) are_congruent_mod m . i by A32, A37, A39, INT_1:16; :: thesis: verum

end;

case A40: k + 1 > i ; :: thesis: Sum (v (#) cc),(u . i) + 0 are_congruent_mod m . i

then k >= i by NAT_1:13;
then A41: Sum ((u | k) (#) (c | k)),u . i are_congruent_mod m . i by A7;
A42: v . (k + 1),v . (k + 1) are_congruent_mod m . i by INT_1:11;
cc . (k + 1), 0 are_congruent_mod m . i by A2, A4, A13, A15, A40, Th27;
then (v . (k + 1)) * (cc . (k + 1)),(u . (k + 1)) * 0 are_congruent_mod m . i by A11, A42, INT_1:18;
hence Sum (v (#) cc),(u . i) + 0 are_congruent_mod m . i by A32, A41, INT_1:16; :: thesis: verum

end;

end;

end;

hence ( ( k + 1 < i & Sum (v (#) cc), 0 are_congruent_mod m . i ) or ( k + 1 >= i & Sum (v (#) cc),u . i are_congruent_mod m . i ) ) ; :: thesis: verum

end;

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

end;

A43: dom m = Seg (len u) by A1, FINSEQ_1:def 3;

now :: thesis: for v, cc being INT -valued FinSequence st v = u | 0 & cc = c | 0 & not ( 0 < i & Sum (v (#) cc), 0 are_congruent_mod m . i ) holds
( 0 >= i & Sum (v (#) cc),u . i are_congruent_mod m . i )

let v, cc be INT -valued FinSequence; :: thesis: ( v = u | 0 & cc = c | 0 & not ( 0 < i & Sum (v (#) cc), 0 are_congruent_mod m . i ) implies ( 0 >= i & Sum (v (#) cc),u . i are_congruent_mod m . i ) )
assume that
A44: v = u | 0 and
cc = c | 0 ; :: thesis: ( ( 0 < i & Sum (v (#) cc), 0 are_congruent_mod m . i ) or ( 0 >= i & Sum (v (#) cc),u . i are_congruent_mod m . i ) )
(dom v) /\ (dom cc) = {} by A44;
then dom (v (#) cc) = {} by VALUED_1:def 4;
then v (#) cc = {} ;
hence ( ( 0 < i & Sum (v (#) cc), 0 are_congruent_mod m . i ) or ( 0 >= i & Sum (v (#) cc),u . i are_congruent_mod m . i ) ) by A2, A43, FINSEQ_1:1, INT_1:11, RVSUM_1:72; :: thesis: verum

end;

then A45: S₁[ 0 ] ;
A46: for k being Element of NAT st 0 <= k & k <= len u holds
S₁[k] from INT_1:sch 7(A45, A5);
len u = len c by A1, Def4;
then A47: c | (len u) = c by FINSEQ_1:58;
A48: u = u | (len u) by FINSEQ_1:58;
i <= len u by A2, A43, FINSEQ_1:1;
hence Sum (u (#) c),u . i are_congruent_mod m . i by A46, A48, A47; :: thesis: verum