set ad = (Int-mult-left F_Rat) | [:INT,INT:];
[:INT,INT:] c= [:INT,RAT:] by NUMBERS:14, ZFMISC_1:96;
then A2: [:INT,INT:] c= dom (Int-mult-left F_Rat) by FUNCT_2:def 1;
A3: dom (Int-mult-left INT.Ring) = [:INT,INT:] by FUNCT_2:def 1;
for z being object st z in dom ((Int-mult-left F_Rat) | [:INT,INT:]) holds
((Int-mult-left F_Rat) | [:INT,INT:]) . z = (Int-mult-left INT.Ring) . z

proof

let z be object ; :: thesis: ( z in dom ((Int-mult-left F_Rat) | [:INT,INT:]) implies ((Int-mult-left F_Rat) | [:INT,INT:]) . z = (Int-mult-left INT.Ring) . z )
assume A4: z in dom ((Int-mult-left F_Rat) | [:INT,INT:]) ; :: thesis: ((Int-mult-left F_Rat) | [:INT,INT:]) . z = (Int-mult-left INT.Ring) . z
then consider x, y being object such that
A5: ( x in INT & y in INT & z = [x,y] ) by ZFMISC_1:def 2;
reconsider x1 = x, y1 = y as Element of INT.Ring by A5;
reconsider y2 = y1 as Element of F_Rat by RAT_1:def 2;
reconsider y3 = y1 as Element of INT.Ring ;
thus ((Int-mult-left F_Rat) | [:INT,INT:]) . z = (Int-mult-left F_Rat) . (x1,y1) by A4, A5, FUNCT_1:49
.= x1 * y2 by ZMODUL07:15
.= (Int-mult-left INT.Ring) . (x1,y3) by ZMODUL06:14
.= (Int-mult-left INT.Ring) . z by A5 ; :: thesis: verum

end;

hence (Int-mult-left F_Rat) | [:INT,INT:] = Int-mult-left INT.Ring by A2, A3, FUNCT_1:2, RELAT_1:62; :: thesis: verum