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 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 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: ( meet (rng a) c= p implies ex i being object st
( i in dom a & a . i c= p ) )
defpred S₁[ Nat] means 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 );
A1: S₁[1] by Th4;
A2: for n being non zero Nat st S₁[n] holds
S₁[n + 1]

proof

let n be non zero Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
for a being non empty FinSequence of Ideals A
for p being prime Ideal of A st len a = n + 1 & meet (rng a) c= p holds
ex i being object st
( i in dom a & a . i c= p )

proof

let a be non empty FinSequence of Ideals A; :: thesis: for p being prime Ideal of A st len a = n + 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 = n + 1 & meet (rng a) c= p implies ex i being object st
( i in dom a & a . i c= p ) )
assume A4: len a = n + 1 ; :: thesis: ( not meet (rng a) c= p or ex i being object st
( i in dom a & a . i c= p ) )
then A5: a = (a | n) ^ <*(a /. (n + 1))*> by FINSEQ_5:21;
A6: len (a | n) = n by A4, FINSEQ_1:59, NAT_1:11;
reconsider an = a | n as non empty FinSequence of Ideals A ;
A7: dom an = Seg (len an) by FINSEQ_1:def 3
.= Seg n by A4, FINSEQ_1:59, NAT_1:11 ;
A8: dom a = Seg (n + 1) by A4, FINSEQ_1:def 3;
A9: ( rng an <> {} & rng <*(a /. (n + 1))*> <> {} ) by RELAT_1:41;
A10: meet (rng a) = meet ((rng an) \/ (rng <*(a /. (n + 1))*>)) by FINSEQ_1:31, A5
.= (meet (rng an)) /\ (meet (rng <*(a /. (n + 1))*>)) by A9, SETFAM_1:9 ;
( meet (rng a) c= p implies ex i being object st
( i in dom a & a . i c= p ) )

proof

assume A11: meet (rng a) c= p ; :: thesis: ex i being object st
( i in dom a & a . i c= p )
reconsider I1 = meet (rng an) as Ideal of A by Th3;
reconsider I2 = meet (rng <*(a /. (n + 1))*>) as Ideal of A by Th3;

per cases ( I1 c= p or I2 c= p ) by Th1, A11, A10;

suppose I1 c= p ; :: thesis: ex i being object st
( i in dom a & a . i c= p )

then consider i being object such that
A13: ( i in dom an & an . i c= p ) by A6, A3;
A14: a . i c= p by A13, A5, FINSEQ_1:def 7;
A15: Seg n c= Seg (n + 1) by FINSEQ_1:5, NAT_1:11;
consider i1 being object such that
A16: i1 = i and
A17: ( i1 in dom a & a . i c= p ) by A14, A13, A7, A8, A15;
thus ex i being object st
( i in dom a & a . i c= p ) by A16, A17; :: thesis: verum

end;

suppose A18: I2 c= p ; :: thesis: ex i being object st
( i in dom a & a . i c= p )

rng <*(a /. (n + 1))*> = {(a /. (n + 1))} by FINSEQ_1:39;
then A19: meet (rng <*(a /. (n + 1))*>) = a /. (n + 1) by SETFAM_1:10
.= a . (n + 1) by A8, FINSEQ_1:4, PARTFUN1:def 6 ;
consider i being object such that
i = n + 1 and
A20: ( i in dom a & a . i c= p ) by A18, A19, A8, FINSEQ_1:4;
thus ex i being object st
( i in dom a & a . i c= p ) by A20; :: thesis: verum

end;

end;

end;

hence ( not meet (rng a) c= p or ex i being object st
( i in dom a & a . i c= p ) ) ; :: thesis: verum

end;

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

end;

A21: for i being non zero Nat holds S₁[i] from NAT_1:sch 10(A1, A2);
reconsider n = len a as non zero Nat ;
n = len a ;
hence ( meet (rng a) c= p implies ex i being object st
( i in dom a & a . i c= p ) ) by A21; :: thesis: verum