let f1, f2 be Function of [: the carrier of INT.Ring, the carrier of AG:], the carrier of AG; :: thesis: ( ( for i being Element of INT.Ring
for a being Element of AG holds
( ( i >= 0 implies f1 . (i,a) = (Nat-mult-left AG) . (i,a) ) & ( i < 0 implies f1 . (i,a) = (Nat-mult-left AG) . ((- i),(- a)) ) ) ) & ( for i being Element of INT.Ring
for a being Element of AG holds
( ( i >= 0 implies f2 . (i,a) = (Nat-mult-left AG) . (i,a) ) & ( i < 0 implies f2 . (i,a) = (Nat-mult-left AG) . ((- i),(- a)) ) ) ) implies f1 = f2 )
assume A4: for i being Element of INT.Ring
for a being Element of AG holds
( ( i >= 0 implies f1 . (i,a) = (Nat-mult-left AG) . (i,a) ) & ( i < 0 implies f1 . (i,a) = (Nat-mult-left AG) . ((- i),(- a)) ) ) ; :: thesis: ( ex i being Element of INT.Ring ex a being Element of AG st
( ( i >= 0 implies f2 . (i,a) = (Nat-mult-left AG) . (i,a) ) implies ( i < 0 & not f2 . (i,a) = (Nat-mult-left AG) . ((- i),(- a)) ) ) or f1 = f2 )
assume A5: for i being Element of INT.Ring
for a being Element of AG holds
( ( i >= 0 implies f2 . (i,a) = (Nat-mult-left AG) . (i,a) ) & ( i < 0 implies f2 . (i,a) = (Nat-mult-left AG) . ((- i),(- a)) ) ) ; :: thesis: f1 = f2
for x, y being set st x in INT & y in the carrier of AG holds
f1 . (x,y) = f2 . (x,y)

proof

let x, y be set ; :: thesis: ( x in INT & y in the carrier of AG implies f1 . (x,y) = f2 . (x,y) )
assume A6: ( x in INT & y in the carrier of AG ) ; :: thesis: f1 . (x,y) = f2 . (x,y)
then reconsider x0 = x as Element of INT ;
reconsider x1 = x as Element of INT.Ring by A6;
reconsider y0 = y as Element of AG by A6;

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

suppose A7: 0 <= x0 ; :: thesis: f1 . (x,y) = f2 . (x,y)

hence f1 . (x,y) = (Nat-mult-left AG) . (x0,y0) by A4
.= f2 . (x,y) by A5, A7 ;
:: thesis: verum

end;

suppose A8: 0 > x0 ; :: thesis: f1 . (x,y) = f2 . (x,y)

hence f1 . (x,y) = (Nat-mult-left AG) . ((- x1),(- y0)) by A4
.= f2 . (x,y) by A5, A8 ;
:: thesis: verum

end;

end;

end;

hence f1 = f2 ; :: thesis: verum