let A be non degenerated commutative Ring; :: thesis: for a being Element of A
for m being maximal Ideal of A st a in ([#] A) \ m holds
({a} -Ideal) + m = [#] A
let a be Element of A; :: thesis: for m being maximal Ideal of A st a in ([#] A) \ m holds
({a} -Ideal) + m = [#] A
let m be maximal Ideal of A; :: thesis: ( a in ([#] A) \ m implies ({a} -Ideal) + m = [#] A )
assume A1: a in ([#] A) \ m ; :: thesis: ({a} -Ideal) + m = [#] A
A2: a in {a} -Ideal by IDEAL_1:66;
0. A in m by IDEAL_1:3;
then A4: a + (0. A) in { (x + y) where x, y is Element of A : ( x in {a} -Ideal & y in m ) } by A2;
reconsider a = a as Element of A ;
A5: a in ({a} -Ideal) + m by A4, IDEAL_1:def 19;
( ({a} -Ideal) + m = m or not ({a} -Ideal) + m is proper ) by IDEAL_1:74, RING_1:def 3;
hence ({a} -Ideal) + m = [#] A by A1, A5, XBOOLE_0:def 5; :: thesis: verum