set ad = addrat || INT;
[:INT,INT:] c= [:RAT,RAT:] by NUMBERS:14, ZFMISC_1:96;
then A1: [:INT,INT:] c= dom addrat by FUNCT_2:def 1;
then A2: dom (addrat || INT) = [:INT,INT:] by RELAT_1:62;
A3: dom addint = [:INT,INT:] by FUNCT_2:def 1;
for z being object st z in dom (addrat || INT) holds
(addrat || INT) . z = addint . z

proof

let z be object ; :: thesis: ( z in dom (addrat || INT) implies (addrat || INT) . z = addint . z )
assume A4: z in dom (addrat || INT) ; :: thesis: (addrat || INT) . z = addint . z
then consider x, y being object such that
A5: ( x in INT & y in INT & z = [x,y] ) by A2, ZFMISC_1:def 2;
reconsider x1 = x, y1 = y as Integer by A5;
thus (addrat || INT) . z = addrat . (x1,y1) by A4, A5, A2, FUNCT_1:49
.= x1 + y1 by BINOP_2:def 15
.= addint . (x1,y1) by BINOP_2:def 20
.= addint . z by A5 ; :: thesis: verum

end;

hence addrat || INT = addint by A1, A3, RELAT_1:62; :: thesis: verum