let u be integer-valued FinSequence; :: thesis: for m being CR_Sequence st dom u = dom m holds
for z being Nat st z solves_CRT u,m & ( for i being Nat st i in dom u holds
u . i,m . i are_coprime ) holds
z, Product m are_coprime
let m be CR_Sequence; :: thesis: ( dom u = dom m implies for z being Nat st z solves_CRT u,m & ( for i being Nat st i in dom u holds
u . i,m . i are_coprime ) holds
z, Product m are_coprime )
assume A1: dom u = dom m ; :: thesis: for z being Nat st z solves_CRT u,m & ( for i being Nat st i in dom u holds
u . i,m . i are_coprime ) holds
z, Product m are_coprime
let z be Nat; :: thesis: ( z solves_CRT u,m & ( for i being Nat st i in dom u holds
u . i,m . i are_coprime ) implies z, Product m are_coprime )
assume that
A2: z solves_CRT u,m and
A3: for i being Nat st i in dom u holds
u . i,m . i are_coprime ; :: thesis: z, Product m are_coprime
rng m c= NAT

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng m or y in NAT )
assume y in rng m ; :: thesis: y in NAT
then consider x being object such that
A4: ( x in dom m & m . x = y ) by FUNCT_1:def 3;
reconsider x = x as Nat by A4;
m . x in NAT ;
hence y in NAT by A4; :: thesis: verum

end;

then A5: m is FinSequence of NAT by FINSEQ_1:def 4;
for i being Nat st i in dom m holds
(m . i) gcd z = 1

proof

let i be Nat; :: thesis: ( i in dom m implies (m . i) gcd z = 1 )
assume A6: i in dom m ; :: thesis: (m . i) gcd z = 1
u . i,m . i are_coprime by A1, A3, A6;
then z,m . i are_coprime by A1, A2, A6, Th5;
hence (m . i) gcd z = 1 ; :: thesis: verum

end;

hence z, Product m are_coprime by A5, WSIERP_1:36; :: thesis: verum