reconsider f = the multF of R || I as Function of [:I,I:], the carrier of R by FUNCT_2:32;
A1: dom f = [:I,I:] by FUNCT_2:def 1;
for x being object st x in [:I,I:] holds
f . x in I

let x be object ; :: thesis:
assume x in [:I,I:] ; :: thesis:
then consider u, v being object such that
A2: ( u in I & v in I ) and
A3: x = [u,v] by ZFMISC_1:def 2;
reconsider u = u, v = v as Element of I by A2;
f . x = the multF of R . [u,v] by A1, A3, FUNCT_1:47
.= u * v ;
hence f . x in I by Def3; :: thesis:

end;