set c = the carrier of G;

defpred S_{1}[ 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_{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 G,(SymGroup the carrier of G) st

for g being Element of G holds b_{1} . g = * g
; :: thesis: verum

defpred S

A1: for x being Element of G ex y being Element of (SymGroup the carrier of G) st S

proof

ex f being Function of G,(SymGroup the carrier of G) st
let x be Element of G; :: thesis: ex y being Element of (SymGroup the carrier of G) st S_{1}[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_{1}[x,y]

thus S_{1}[x,y]
; :: thesis: verum

end;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

thus S

for x being Element of G holds S

hence ex b

for g being Element of G holds b