let A be non degenerated commutative Ring; :: thesis:
let q be Ideal of A; :: thesis:
A1: for x1, x2 being object st x1 in dom (Psi q) & x2 in dom (Psi q) & (Psi q) . x1 = (Psi q) . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis:
assume A2: ( x1 in dom (Psi q) & x2 in dom (Psi q) & (Psi q) . x1 = (Psi q) . x2 ) ; :: thesis:
then A3: ( x1 in Ideals (A / q) & x2 in Ideals (A / q) ) ;
then A4: x1 in { I where I is Ideal of (A / q) : verum } by RING_2:def 3;
x2 in { I where I is Ideal of (A / q) : verum } by A3, RING_2:def 3;
then consider z2 being Ideal of (A / q) such that
A5: z2 = x2 ;
consider z1 being Ideal of (A / q) such that
A6: z1 = x1 by A4;
A7: (canHom q) " z1 = (Psi q) . x2 by A2, Def3, A6
.= (canHom q) " z2 by A2, A5, Def3 ;
z1 = (canHom q) .: ((canHom q) " z2) by A7, Th24
.= z2 by Th24 ;
hence x1 = x2 by A5, A6; :: thesis:

end;

for x1, x2 being set st x1 in dom (Psi q) & x2 in dom (Psi q) & x1 c= x2 holds
(Psi q) . x1 c= (Psi q) . x2

let x1, x2 be set ; :: thesis:
assume A10: ( x1 in dom (Psi q) & x2 in dom (Psi q) & x1 c= x2 ) ; :: thesis:
then A11: ( x1 in Ideals (A / q) & x2 in Ideals (A / q) ) ;
then A12: x1 in { I where I is Ideal of (A / q) : verum } by RING_2:def 3;
x2 in { I where I is Ideal of (A / q) : verum } by A11, RING_2:def 3;
then consider z2 being Ideal of (A / q) such that
A13: z2 = x2 ;
consider z1 being Ideal of (A / q) such that
A14: z1 = x1 by A12;
A15: (canHom q) " z1 = (Psi q) . x1 by A10, Def3, A14;
(canHom q) " z2 = (Psi q) . x2 by A10, A13, Def3;
hence (Psi q) . x1 c= (Psi q) . x2 by A15, A10, A13, A14, Th27; :: thesis:

end;