P is RingEpimorphism by A1;
then A3: P is onto ;
let I be Ideal of S; :: thesis: I is finitely_generated
P is RingMonomorphism by A1;
then A4: P is one-to-one ;
reconsider PI = (P ") .: I as Ideal of R by A1, Th22, Th25;
PI is finitely_generated by A2;
then consider F being non empty finite Subset of R such that
A5: (P ") .: I = F -Ideal ;
P is onto by A3;
then P " = P " by A4, TOPS_2:def 4;
then P .: ((P ") .: I) = P .: (P " I) by A4, FUNCT_1:85;
then P .: ((P ") .: I) = I by A3, FUNCT_1:77;
then I = (P .: F) -Ideal by A1, A5, Th26;
hence I is finitely_generated ; :: thesis: verum