defpred S₁[ object , object ] means ex a being Element of G st
( $1 = a & $2 = a * N );
A1: for x being object st x in the carrier of G holds
ex y being object st S₁[x,y]

proof

let x be object ; :: thesis: ( x in the carrier of G implies ex y being object st S₁[x,y] )
assume x in the carrier of G ; :: thesis: ex y being object st S₁[x,y]
then reconsider a = x as Element of G ;
reconsider y = a * N as set ;
take y ; :: thesis: S₁[x,y]
take a ; :: thesis: ( x = a & y = a * N )
thus ( x = a & y = a * N ) ; :: thesis: verum

end;

consider f being Function such that
A2: dom f = the carrier of G and
A3: for x being object st x in the carrier of G holds
S₁[x,f . x] from CLASSES1:sch 1(A1);
rng f c= the carrier of (G ./. N)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in the carrier of (G ./. N) )
assume x in rng f ; :: thesis: x in the carrier of (G ./. N)
then consider y being object such that
A4: y in dom f and
A5: f . y = x by FUNCT_1:def 3;
consider a being Element of G such that
y = a and
A6: f . y = a * N by A2, A3, A4;
a * N = N * a by GROUP_3:117;
then x in G ./. N by A5, A6, Th23;
hence x in the carrier of (G ./. N) ; :: thesis: verum

end;

then reconsider f = f as Function of G,(G ./. N) by A2, FUNCT_2:def 1, RELSET_1:4;
take f ; :: thesis: for a being Element of G holds f . a = a * N
let a be Element of G; :: thesis: f . a = a * N
ex b being Element of G st
( a = b & f . a = b * N ) by A3;
hence f . a = a * N ; :: thesis: verum