set c = the carrier of G;
defpred S₁[ Element of G, set ] means $2 = * $1;
A1: for x being Element of G ex y being Element of (SymGroup the carrier of G) st S₁[x,y]

proof

let x be Element of G; :: thesis: ex y being Element of (SymGroup the carrier of G) st S₁[x,y]
set y = * x;
* x in permutations the carrier of G ;
then reconsider y = * x as Element of (SymGroup the carrier of G) by Def2;
take y ; :: thesis: S₁[x,y]
thus S₁[x,y] ; :: thesis: verum

end;

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