let A be non degenerated commutative Ring; :: thesis: for a being non empty FinSequence of Ideals A holds meet (rng a) is Ideal of A
let a be non empty FinSequence of Ideals A; :: thesis: meet (rng a) is Ideal of A
defpred S1[ Nat] means for a being non empty FinSequence of Ideals A st len a = $1 holds
meet (rng a) is Ideal of A;
A1: S1[1]
proof
for a being non empty FinSequence of Ideals A st len a = 1 holds
meet (rng a) is Ideal of A
proof
let a be non empty FinSequence of Ideals A; :: thesis: ( len a = 1 implies meet (rng a) is Ideal of A )
assume A2: len a = 1 ; :: thesis: meet (rng a) is Ideal of A
then {1} = dom a by FINSEQ_1:def 3, FINSEQ_1:2;
then a2: 1 in dom a by FINSEQ_1:2;
then reconsider e = 1 as Element of dom a ;
a = <*(a . 1)*> by A2, FINSEQ_1:40;
then rng a = {(a . 1)} by FINSEQ_1:39;
then meet (rng a) = a . e by SETFAM_1:10;
hence meet (rng a) is Ideal of A ; :: thesis: verum
end;
hence S1[1] ; :: thesis: verum
end;
A5: for n being non zero Nat st S1[n] holds
S1[n + 1]
proof
let n be non zero Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A6: S1[n] ; :: thesis: S1[n + 1]
for a being non empty FinSequence of Ideals A st len a = n + 1 holds
meet (rng a) is Ideal of A
proof
let a be non empty FinSequence of Ideals A; :: thesis: ( len a = n + 1 implies meet (rng a) is Ideal of A )
assume A7: len a = n + 1 ; :: thesis: meet (rng a) is Ideal of A
then A8: a = (a | n) ^ <*(a /. (n + 1))*> by FINSEQ_5:21;
A9: len (a | n) = n by A7, FINSEQ_1:59, NAT_1:11;
reconsider an = a | n as non empty FinSequence of Ideals A ;
reconsider I1 = meet (rng an) as Ideal of A by A6, A9;
A10: dom a = Seg (n + 1) by A7, FINSEQ_1:def 3;
( 1 <= n + 1 & n + 1 <= n + 1 ) by NAT_1:11;
then n + 1 in dom a by A10;
then reconsider n1 = n + 1 as Element of dom a ;
rng <*(a /. (n + 1))*> = {(a /. (n + 1))} by FINSEQ_1:39;
then A12: meet (rng <*(a /. (n + 1))*>) = a /. (n + 1) by SETFAM_1:10
.= a . n1 by A10, PARTFUN1:def 6 ;
reconsider I2 = meet (rng <*(a /. n1)*>) as Ideal of A by A12;
A13: ( rng an <> {} & rng <*(a /. (n + 1))*> <> {} ) by RELAT_1:41;
meet (rng a) = meet ((rng an) \/ (rng <*(a /. (n + 1))*>)) by FINSEQ_1:31, A8
.= I1 /\ I2 by A13, SETFAM_1:9 ;
hence meet (rng a) is Ideal of A ; :: thesis: verum
end;
hence S1[n + 1] ; :: thesis: verum
end;
A15: for i being non zero Nat holds S1[i] from NAT_1:sch 10(A1, A5);
 reconsider n = len a as non zero Nat ;
n = len a ;
hence meet (rng a) is Ideal of A by A15; :: thesis: verum