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

proof

let x be Element of ; :: thesis: ex y being Element of con_class a st S₁[x,y]
a |^ x in con_class a by GROUP_3:97;
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 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 holds b₁ . x = a |^ x ; :: thesis: verum