defpred S₁[ Element of the carrier of INT.Ring, Element of AG, Element of AG] means ( ( $1 >= 0 implies $3 = (Nat-mult-left AG) . ($1,$2) ) & ( $1 < 0 implies $3 = (Nat-mult-left AG) . ((- $1),(- $2)) ) );
A1: for x being Element of the carrier of INT.Ring
for y being Element of AG ex z being Element of AG st S₁[x,y,z]

proof

let x be Element of the carrier of INT.Ring; :: thesis: for y being Element of AG ex z being Element of AG st S₁[x,y,z]
let y be Element of AG; :: thesis: ex z being Element of AG st S₁[x,y,z]
reconsider xx = x as Element of INT ;

per cases ( x >= 0 or x < 0 ) ;

suppose x >= 0 ; :: thesis: ex z being Element of AG st S₁[x,y,z]

then reconsider x0 = x as Element of NAT by INT_1:3;
reconsider z = (Nat-mult-left AG) . (x0,y) as Element of AG ;
S₁[x,y,z] ;
hence ex z being Element of AG st S₁[x,y,z] ; :: thesis: verum

end;

suppose a2: x < 0 ; :: thesis: ex z being Element of AG st S₁[x,y,z]

then reconsider x0 = - xx as Element of NAT by INT_1:3;
reconsider z = (Nat-mult-left AG) . (x0,(- y)) as Element of AG ;
T1: ( x >= 0 implies z = (Nat-mult-left AG) . (x,y) ) by a2;
S₁[x,y,z] by T1;
hence ex z being Element of AG st S₁[x,y,z] ; :: thesis: verum

end;

end;

end;

consider f being Function of [: the carrier of INT.Ring, the carrier of AG:], the carrier of AG such that
A3: for x being Element of the carrier of INT.Ring
for y being Element of the carrier of AG holds S₁[x,y,f . (x,y)] from BINOP_1:sch 3(A1);
take f ; :: thesis: for i being Element of INT.Ring
for a being Element of AG holds
( ( i >= 0 implies f . (i,a) = (Nat-mult-left AG) . (i,a) ) & ( i < 0 implies f . (i,a) = (Nat-mult-left AG) . ((- i),(- a)) ) )
thus for i being Element of INT.Ring
for a being Element of AG holds
( ( i >= 0 implies f . (i,a) = (Nat-mult-left AG) . (i,a) ) & ( i < 0 implies f . (i,a) = (Nat-mult-left AG) . ((- i),(- a)) ) ) by A3; :: thesis: verum