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

proof

let x be set ; :: thesis: ( x in [:I,I:] implies f . x in I )
assume x in [:I,I:] ; :: thesis: f . x in I
then consider u, v being set such that
A2: ( u in I & v in I & 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, A2, FUNCT_1:70
.= u * v ;
hence f . x in I by Def3; :: thesis: verum

end;

hence the multF of R || I is BinOp of I by A1, FUNCT_2:5; :: thesis: verum