let fp be FinSequence of NAT ; :: thesis: ( len fp >= 2 & ( for b, c being Element of NAT st b in dom fp & c in dom fp & b <> c holds
(fp . b) gcd (fp . c) = 1 ) & ( for b being Element of NAT st b in dom fp holds
fp . b <> 0 ) implies for fp1 being FinSequence of NAT ex x being Integer st
for b being Element of NAT st b in dom fp holds
(x - (fp1 . b)) mod (fp . b) = 0 )
assume that
A1: len fp >= 2 and
A2: for b, c being Element of NAT st b in dom fp & c in dom fp & b <> c holds
(fp . b) gcd (fp . c) = 1 and
A3: for b being Element of NAT st b in dom fp holds
fp . b <> 0 ; :: thesis: for fp1 being FinSequence of NAT ex x being Integer st
for b being Element of NAT st b in dom fp holds
(x - (fp1 . b)) mod (fp . b) = 0
consider fp2 being FinSequence of NAT , q being Element of NAT such that
A4: fp = fp2 ^ <*q*> by A1, FINSEQ_2:19;
deffunc H₁( Nat) -> set = { l where l is Element of NAT : (((Product (Del (fp,$1))) * l) - 1) mod (fp . $1) = 0 } ;
defpred S₁[ Nat, Nat] means $2 in H₁($1);
A5: for a being Nat st a in Seg (len fp) holds
ex n being Element of NAT st S₁[a,n]

proof

let a be Nat; :: thesis: ( a in Seg (len fp) implies ex n being Element of NAT st S₁[a,n] )
reconsider l = fp . a as Integer ;
assume a in Seg (len fp) ; :: thesis: ex n being Element of NAT st S₁[a,n]
then A6: a in dom fp by FINSEQ_1:def 3;
then (Product (Del (fp,a))) gcd (fp . a) = 1 by A1, A2, Th31;
then A7: Product (Del (fp,a)),l are_relative_prime by INT_2:def 3;
l <> 0 by A3, A6;
then consider n being Nat such that
A8: (((Product (Del (fp,a))) * n) - 1) mod l = 0 by A7, Th16;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
take n ; :: thesis: S₁[a,n]
thus S₁[a,n] by A8; :: thesis: verum

end;

consider s being FinSequence of NAT such that
A9: ( dom s = Seg (len fp) & ( for a being Nat st a in Seg (len fp) holds
S₁[a,s . a] ) ) from FINSEQ_1:sch 5(A5);
let fp1 be FinSequence of NAT ; :: thesis: ex x being Integer st
for b being Element of NAT st b in dom fp holds
(x - (fp1 . b)) mod (fp . b) = 0
set k = len fp2;
deffunc H₂( Nat) -> Element of REAL = ((Product (Del (fp,$1))) * (s . $1)) * (fp1 . $1);
consider s1 being FinSequence such that
A10: ( len s1 = (len fp2) + 1 & ( for a being Nat st a in dom s1 holds
s1 . a = H₂(a) ) ) from FINSEQ_1:sch 2();
for a being Nat st a in dom s1 holds
s1 . a in NAT

proof

let a be Nat; :: thesis: ( a in dom s1 implies s1 . a in NAT )
assume A11: a in dom s1 ; :: thesis: s1 . a in NAT
reconsider a = a as Element of NAT by ORDINAL1:def 12;
s1 . a = ((Product (Del (fp,a))) * (s . a)) * (fp1 . a) by A10, A11;
hence s1 . a in NAT by ORDINAL1:def 12; :: thesis: verum

end;

then reconsider s1 = s1 as FinSequence of NAT by FINSEQ_2:12;
set x = Sum s1;
take Sum s1 ; :: thesis: for b being Element of NAT st b in dom fp holds
((Sum s1) - (fp1 . b)) mod (fp . b) = 0
A12: len fp = (len fp2) + 1 by A4, FINSEQ_2:16;
A13: for a being Nat
for b being Element of NAT st a in dom fp & b in dom fp & a <> b holds
fp . b divides s1 . a

proof

let a be Nat; :: thesis: for b being Element of NAT st a in dom fp & b in dom fp & a <> b holds
fp . b divides s1 . a
let b be Element of NAT ; :: thesis: ( a in dom fp & b in dom fp & a <> b implies fp . b divides s1 . a )
assume that
A14: a in dom fp and
A15: ( b in dom fp & a <> b ) ; :: thesis: fp . b divides s1 . a
len fp >= 1 by A1, XXREAL_0:2;
then fp . b divides (Product (Del (fp,a))) * ((s . a) * (fp1 . a)) by A14, A15, Th35, NAT_D:9;
then A16: fp . b divides ((Product (Del (fp,a))) * (s . a)) * (fp1 . a) ;
a in dom s1 by A12, A10, A14, FINSEQ_3:29;
hence fp . b divides s1 . a by A10, A16; :: thesis: verum

end;

A17: for b being Element of NAT st b in dom fp holds
fp . b divides Sum (Del (s1,b))

proof

let b be Element of NAT ; :: thesis: ( b in dom fp implies fp . b divides Sum (Del (s1,b)) )
assume A18: b in dom fp ; :: thesis: fp . b divides Sum (Del (s1,b))
then b in Seg (len s1) by A12, A10, FINSEQ_1:def 3;
then A19: b in dom s1 by FINSEQ_1:def 3;
then A20: (len (Del (s1,b))) + 1 = (len fp2) + 1 by A10, WSIERP_1:def 1;
for a being Nat st a in dom (Del (s1,b)) holds
fp . b divides (Del (s1,b)) . a

proof

let a be Nat; :: thesis: ( a in dom (Del (s1,b)) implies fp . b divides (Del (s1,b)) . a )
assume A21: a in dom (Del (s1,b)) ; :: thesis: fp . b divides (Del (s1,b)) . a
then A22: ( a >= 1 & a <= len fp2 ) by A20, FINSEQ_3:25;
dom (Del (s1,b)) c= dom s1 by WSIERP_1:39;
then a in dom s1 by A21;
then a in Seg ((len fp2) + 1) by A10, FINSEQ_1:def 3;
then A23: a in dom fp by A12, FINSEQ_1:def 3;

per cases ( a < b or a >= b ) ;

suppose A24: a < b ; :: thesis: fp . b divides (Del (s1,b)) . a

then (Del (s1,b)) . a = s1 . a by A19, WSIERP_1:def 1;
hence fp . b divides (Del (s1,b)) . a by A13, A18, A23, A24; :: thesis: verum

end;

suppose A25: a >= b ; :: thesis: fp . b divides (Del (s1,b)) . a

( a + 1 <= (len fp2) + 1 & a + 1 > 1 ) by A22, XREAL_1:6, XREAL_1:29;
then A26: a + 1 in dom fp by A12, FINSEQ_3:25;
( (Del (s1,b)) . a = s1 . (a + 1) & a + 1 > b ) by A19, A25, WSIERP_1:def 1, XREAL_1:39;
hence fp . b divides (Del (s1,b)) . a by A13, A18, A26; :: thesis: verum

end;

end;

end;

hence fp . b divides Sum (Del (s1,b)) by Th36; :: thesis: verum

end;

for b being Element of NAT st b in dom fp holds
((Sum s1) - (fp1 . b)) mod (fp . b) = 0

proof

let b be Element of NAT ; :: thesis: ( b in dom fp implies ((Sum s1) - (fp1 . b)) mod (fp . b) = 0 )
assume A27: b in dom fp ; :: thesis: ((Sum s1) - (fp1 . b)) mod (fp . b) = 0
then A28: fp . b <> 0 by A3;
A29: fp . b divides Sum (Del (s1,b)) by A17, A27;
A30: ((Sum (Del (s1,b))) + ((s1 . b) - (fp1 . b))) mod (fp . b) = ((s1 . b) - (fp1 . b)) mod (fp . b)

proof

reconsider l = Sum (Del (s1,b)) as Integer ;
A31: l mod (fp . b) = 0 by A29, A28, INT_1:62;
((Sum (Del (s1,b))) + ((s1 . b) - (fp1 . b))) mod (fp . b) = ((l mod (fp . b)) + (((s1 . b) - (fp1 . b)) mod (fp . b))) mod (fp . b) by NAT_D:66
.= ((s1 . b) - (fp1 . b)) mod (fp . b) by A31, NAT_D:65 ;
hence ((Sum (Del (s1,b))) + ((s1 . b) - (fp1 . b))) mod (fp . b) = ((s1 . b) - (fp1 . b)) mod (fp . b) ; :: thesis: verum

end;

A32: ( b >= 1 & b <= (len fp2) + 1 ) by A12, A27, FINSEQ_3:25;
then A33: b in Seg ((len fp2) + 1) ;
then b in dom s1 by A10, FINSEQ_1:def 3;
then A34: (s1 . b) - (fp1 . b) = (((Product (Del (fp,b))) * (s . b)) * (fp1 . b)) - (1 * (fp1 . b)) by A10
.= (((Product (Del (fp,b))) * (s . b)) - 1) * (fp1 . b) ;
s . b in H₁(b) by A12, A9, A33;
then A35: ex ll being Element of NAT st
( ll = s . b & (((Product (Del (fp,b))) * ll) - 1) mod (fp . b) = 0 ) ;
b in dom s1 by A10, A32, FINSEQ_3:25;
then ((Sum s1) - (fp1 . b)) mod (fp . b) = (((Sum (Del (s1,b))) + (s1 . b)) - (fp1 . b)) mod (fp . b) by WSIERP_1:20
.= 0 by A28, A34, A35, A30, Lm9 ;
hence ((Sum s1) - (fp1 . b)) mod (fp . b) = 0 ; :: thesis: verum

end;

hence for b being Element of NAT st b in dom fp holds
((Sum s1) - (fp1 . b)) mod (fp . b) = 0 ; :: thesis: verum