let F be Field; :: thesis: F is Noetherian
let I be Ideal of F; :: according to IDEAL_1:def 26 :: thesis: I is finitely_generated
per cases ( I = {(0. F)} or I = the carrier of F ) by IDEAL_1:22;
suppose A1: I = {(0. F)} ; :: thesis: I is finitely_generated
reconsider s0F = {(0. F)} as non empty finite Subset of F ;
{(0. F)} = s0F -Ideal by IDEAL_1:47;
hence I is finitely_generated by A1; :: thesis: verum
end;
suppose A2: I = the carrier of F ; :: thesis: I is finitely_generated
reconsider s1F = {(1_ F)} as non empty finite Subset of F ;
the carrier of F = s1F -Ideal by IDEAL_1:51;
hence I is finitely_generated by A2; :: thesis: verum
end;
end;