let R be Ring; :: thesis: for I being Subset of R holds
( I is Ideal of R iff ex S being R -homomorphic Ring ex f being Homomorphism of R,S st ker f = I )
let I be Subset of R; :: thesis: ( I is Ideal of R iff ex S being R -homomorphic Ring ex f being Homomorphism of R,S st ker f = I )

now :: thesis: ( I is Ideal of R implies ex S being R -homomorphic Ring ex f being Homomorphism of R,S st ker f = I )

assume A: I is Ideal of R ; :: thesis: ex S being R -homomorphic Ring ex f being Homomorphism of R,S st ker f = I
thus ex S being R -homomorphic Ring ex f being Homomorphism of R,S st ker f = I :: thesis: verum

proof

reconsider I = I as Ideal of R by A;
take R / I ; :: thesis: ex f being Homomorphism of R,(R / I) st ker f = I
take canHom I ; :: thesis: ker (canHom I) = I
thus ker (canHom I) = I by kercanhomI; :: thesis: verum

end;

end;

hence ( I is Ideal of R iff ex S being R -homomorphic Ring ex f being Homomorphism of R,S st ker f = I ) ; :: thesis: verum