defpred S_{1}[ 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_{1}[x,y]

for x being Element of G holds S_{1}[x,f . x]
from FUNCT_2:sch 3(A1);

hence ex b_{1} being Function of the carrier of G,(con_class a) st

for x being Element of G holds b_{1} . x = a |^ x
; :: thesis: verum

A1: for x being Element of G ex y being Element of con_class a st S

proof

ex f being Function of the carrier of G,(con_class a) st
let x be Element of G; :: thesis: ex y being Element of con_class a st S_{1}[x,y]

a |^ x in con_class a by GROUP_3:82;

hence ex y being Element of con_class a st S_{1}[x,y]
; :: thesis: verum

end;a |^ x in con_class a by GROUP_3:82;

hence ex y being Element of con_class a st S

for x being Element of G holds S

hence ex b

for x being Element of G holds b