defpred S₁[ Element of G, set ] means $2 = a |^ $1;
A1: for x being Element of G ex y being Element of con_class a st S₁[x,y]

proof

let x be Element of G; :: thesis: ex y being Element of con_class a st S₁[x,y]
a |^ x in con_class a by GROUP_3:82;
hence ex y being Element of con_class a st S₁[x,y] ; :: thesis: verum

end;

ex f being Function of the carrier of G,(con_class a) st
for x being Element of G holds S₁[x,f . x] from FUNCT_2:sch 3(A1);
hence ex b₁ being Function of the carrier of G,(con_class a) st
for x being Element of G holds b₁ . x = a |^ x ; :: thesis: verum