let A be non degenerated commutative Ring; :: thesis: for I being proper Ideal of A
for F being non empty FinSequence of Ideals A holds
( rng ((% I) * F) <> {} & rng F <> {} & meet (rng ((% I) * F)) c= the carrier of A )
let I be proper Ideal of A; :: thesis: for F being non empty FinSequence of Ideals A holds
( rng ((% I) * F) <> {} & rng F <> {} & meet (rng ((% I) * F)) c= the carrier of A )
let F be non empty FinSequence of Ideals A; :: thesis: ( rng ((% I) * F) <> {} & rng F <> {} & meet (rng ((% I) * F)) c= the carrier of A )
reconsider J = meet (rng F) as Ideal of A by Th3;
A1: rng F c= bool the carrier of A by XBOOLE_1:1;
then reconsider F1 = F as non empty FinSequence of bool the carrier of A by FINSEQ_1:def 4;
A2: dom (% I) = bool the carrier of A by FUNCT_2:def 1;
A3: 1 in dom F by FINSEQ_5:6;
1 in dom ((% I) * F) by A1, A2, RELAT_1:27, A3;
hence ( rng ((% I) * F) <> {} & rng F <> {} & meet (rng ((% I) * F)) c= the carrier of A ) by A3, FUNCT_1:3; :: thesis: verum