let A be non degenerated commutative Ring; :: thesis: for q being Ideal of A
for M being Ideal of (A / q) st M is proper holds
(canHom q) " M is proper
let q be Ideal of A; :: thesis: for M being Ideal of (A / q) st M is proper holds
(canHom q) " M is proper
let M be Ideal of (A / q); :: thesis: ( M is proper implies (canHom q) " M is proper )
assume A1: M is proper ; :: thesis: (canHom q) " M is proper
assume not (canHom q) " M is proper ; :: thesis: contradiction
then M = (canHom q) .: ([#] A) by Th24
.= (canHom q) .: (dom (canHom q)) by FUNCT_2:def 1
.= rng (canHom q) by RELAT_1:113
.= [#] (A / q) by FUNCT_2:def 3 ;
hence contradiction by A1; :: thesis: verum