let A be non degenerated commutative Ring; :: thesis: for a being non empty FinSequence of Ideals A
for p being prime Ideal of A st len a = 1 & meet (rng a) c= p holds
ex i being object st
( i in dom a & a . i c= p )
let a be non empty FinSequence of Ideals A; :: thesis: for p being prime Ideal of A st len a = 1 & meet (rng a) c= p holds
ex i being object st
( i in dom a & a . i c= p )
let p be prime Ideal of A; :: thesis: ( len a = 1 & meet (rng a) c= p implies ex i being object st
( i in dom a & a . i c= p ) )
assume A1: len a = 1 ; :: thesis: ( not meet (rng a) c= p or ex i being object st
( i in dom a & a . i c= p ) )
then A2: {1} = dom a by FINSEQ_1:def 3, FINSEQ_1:2;
a = <*(a . 1)*> by A1, FINSEQ_1:40;
then A4: rng a = {(a . 1)} by FINSEQ_1:39;
assume A5: meet (rng a) c= p ; :: thesis: ex i being object st
( i in dom a & a . i c= p )
consider i being object such that
A6: i in dom a by A2, XBOOLE_0:def 1;
reconsider i = i as Nat by A6;
a . i = a . 1 by A6, A2, TARSKI:def 1
.= meet (rng a) by A4, SETFAM_1:10 ;
hence ex i being object st
( i in dom a & a . i c= p ) by A5, A6; :: thesis: verum