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

proof

let x be set ; :: thesis: ( x in the carrier of G implies ex y being set st S₁[x,y] )
assume x in the carrier of G ; :: thesis: ex y being set 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 set 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 set ; :: 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 set 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, Th28;
hence x in the carrier of (G ./. N) by STRUCT_0:def 5; :: thesis: verum

end;

then reconsider f = f as Function of G,(G ./. N) by A2, FUNCT_2:def 1, RELSET_1:4;

now

let a, b be Element of G; :: thesis: (f . a) * (f . b) = f . (a * b)
consider a1 being Element of G such that
A7: a = a1 and
A8: f . a = a1 * N by A3;
consider b1 being Element of G such that
A9: b = b1 and
A10: f . b = b1 * N by A3;
A11: ex c being Element of G st
( c = a * b & f . (a * b) = c * N ) by A3;
thus (f . a) * (f . b) = (@ (f . a)) * (@ (f . b)) by Def4
.= ((a1 * N) * b1) * N by A8, A10, GROUP_3:9
.= (a1 * (N * b1)) * N by GROUP_2:106
.= (a1 * (b1 * N)) * N by GROUP_3:117
.= a1 * ((b1 * N) * N) by GROUP_2:96
.= a1 * (b1 * N) by Th6
.= f . (a * b) by A7, A9, A11, GROUP_2:105 ; :: thesis: verum

end;

then reconsider f = f as Homomorphism of G,(G ./. N) by Def7;
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