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 ;
( 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:])
;
((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
;
verum
end;
hence
(Int-mult-left F_Rat) | [:INT,INT:] = Int-mult-left INT.Ring
by A2, A3, FUNCT_1:2, RELAT_1:62; verum