defpred S₁[ object , object ] means ex z being G_INTEG st
( $1 = z & $2 = Norm z );
A1: for x being Element of the carrier of Gauss_INT_Ring ex y being Element of NAT st S₁[x,y]

proof

let x be Element of the carrier of Gauss_INT_Ring; :: thesis: ex y being Element of NAT st S₁[x,y]
reconsider z = x as G_INTEG by Th2;
Norm z is Element of NAT by ORDINAL1:def 12;
hence ex y being Element of NAT st S₁[x,y] ; :: thesis: verum

end;

consider f being Function of Gauss_INT_Ring,NAT such that
A2: for x being Element of Gauss_INT_Ring holds S₁[x,f . x] from FUNCT_2:sch 3(A1);

now :: thesis: for x being G_INTEG holds f . x = Norm x

let x be G_INTEG; :: thesis: f . x = Norm x
x is Element of the carrier of Gauss_INT_Ring by Th3;
then ex z being G_INTEG st
( x = z & f . x = Norm z ) by A2;
hence f . x = Norm x ; :: thesis: verum

end;

hence ex f being Function of Gauss_INT_Ring,NAT st
for x being G_INTEG holds f . x = Norm x ; :: thesis: verum