defpred S₁[ Element of Ideals (A / q), object ] means $2 = (canHom q) " $1;
A1: for x being Element of Ideals (A / q) ex y being Element of Ideals (A,q) st S₁[x,y]

proof

let M be Element of Ideals (A / q); :: thesis: ex y being Element of Ideals (A,q) st S₁[M,y]
A2: M in Ideals (A / q) ;
Ideals (A / q) = { a where a is Ideal of (A / q) : verum } by RING_2:def 3;
then consider J being Ideal of (A / q) such that
A3: J = M by A2;
A4: (canHom q) " J is Ideal of A by Th22;
q c= (canHom q) " J by Th23;
then (canHom q) " J in { I where I is Ideal of A : q c= I } by A4;
then (canHom q) " M in Ideals (A,q) by A3, TOPZARI1:def 1;
hence ex y being Element of Ideals (A,q) st S₁[M,y] ; :: thesis: verum

end;

consider f being Function of (Ideals (A / q)),(Ideals (A,q)) such that
A6: for x being Element of Ideals (A / q) holds S₁[x,f . x] from FUNCT_2:sch 3(A1);
thus ex b₁ being Function of (Ideals (A / q)),(Ideals (A,q)) st
for x being Element of Ideals (A / q) holds b₁ . x = (canHom q) " x by A6; :: thesis: verum