let A be non degenerated commutative Ring; :: thesis: for p being prime Ideal of A
for F being non empty FinSequence of PRIMARY (A,p) holds meet (rng F) in PRIMARY (A,p)
let p be prime Ideal of A; :: thesis: for F being non empty FinSequence of PRIMARY (A,p) holds meet (rng F) in PRIMARY (A,p)
let F be non empty FinSequence of PRIMARY (A,p); :: thesis: meet (rng F) in PRIMARY (A,p)
set q = meet (rng F);
meet (rng F) in PRIMARY (A,p)

proof

A1: len F <> 0 ;
defpred S₁[ Nat] means for F being non empty FinSequence of PRIMARY (A,p) st $1 = len F holds
meet (rng F) in PRIMARY (A,p);
A2: for n being Nat st n >= 1 & S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( n >= 1 & S₁[n] implies S₁[n + 1] )
assume that
A3: n >= 1 and
A4: S₁[n] ; :: thesis: S₁[n + 1]
for F being non empty FinSequence of PRIMARY (A,p) st n + 1 = len F holds
meet (rng F) in PRIMARY (A,p)

proof

let F be non empty FinSequence of PRIMARY (A,p); :: thesis: ( n + 1 = len F implies meet (rng F) in PRIMARY (A,p) )
assume A5: n + 1 = len F ; :: thesis: meet (rng F) in PRIMARY (A,p)
len F <> 0 ;
then consider G being FinSequence of PRIMARY (A,p), q being Element of PRIMARY (A,p) such that
A6: F = G ^ <*q*> by FINSEQ_2:19;
A7: Seg (len <*q*>) = dom <*q*> by FINSEQ_1:def 3
.= Seg 1 by FINSEQ_1:def 8 ;
A8: len F = (len G) + (len <*q*>) by A6, FINSEQ_1:22
.= (len G) + 1 by A7, FINSEQ_1:6 ;
reconsider G = G as non empty FinSequence of PRIMARY (A,p) by A3, A5, A8;
A9: meet (rng G) in PRIMARY (A,p) by A4, A5, A8;
dom G = Seg n by A5, A8, FINSEQ_1:def 3;
then A10: 1 in dom G by A3;
dom <*q*> = Seg 1 by FINSEQ_1:def 8;
then A12: ( rng G <> {} & rng <*q*> <> {} ) by A10, RELAT_1:42;
q in { I where I is primary Ideal of A : I is p -primary } ;
then consider q1 being primary Ideal of A such that
A13: ( q1 = q & q1 is p -primary ) ;
consider q2 being primary Ideal of A such that
A14: ( q2 = meet (rng G) & q2 is p -primary ) by A9;
q2 /\ q1 in { I where I is primary Ideal of A : I is p -primary } by A13, A9, A14, Th41;
then consider q3 being primary Ideal of A such that
A15: q3 = q2 /\ q1 and
A16: q3 is p -primary ;
A17: meet (rng F) = meet ((rng G) \/ (rng <*q*>)) by A6, FINSEQ_1:31
.= (meet (rng G)) /\ (meet (rng <*q*>)) by A12, SETFAM_1:9
.= (meet (rng G)) /\ (meet {q}) by FINSEQ_1:38
.= q3 by A15, A14, A13, SETFAM_1:10 ;
reconsider Q = meet (rng F) as primary Ideal of A by A17;
thus meet (rng F) in PRIMARY (A,p) by A17, A16; :: thesis: verum

end;

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

end;

A18: S₁[1]

proof

for F being non empty FinSequence of PRIMARY (A,p) st 1 = len F holds
meet (rng F) in PRIMARY (A,p)

proof

let F be non empty FinSequence of PRIMARY (A,p); :: thesis: ( 1 = len F implies meet (rng F) in PRIMARY (A,p) )
assume 1 = len F ; :: thesis: meet (rng F) in PRIMARY (A,p)
then A20: dom F = {1} by FINSEQ_1:2, FINSEQ_1:def 3;
then A21: rng F = {(F . 1)} by FUNCT_1:4;
A22: meet (rng F) = meet {(F . 1)} by A20, FUNCT_1:4
.= F . 1 by SETFAM_1:10 ;
F . 1 in {(F . 1)} by TARSKI:def 1;
hence meet (rng F) in PRIMARY (A,p) by A22, A21; :: thesis: verum

end;

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

end;

for n being Nat st n >= 1 holds
S₁[n] from NAT_1:sch 8(A18, A2);
hence meet (rng F) in PRIMARY (A,p) by A1, NAT_1:14; :: thesis: verum

end;

hence meet (rng F) in PRIMARY (A,p) ; :: thesis: verum