reconsider f = the addF 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
proof
let x be
object ;
( x in [:I,I:] implies f . x in I )
assume A2:
x in [:I,I:]
;
f . x in I
then consider u,
v being
object such that A3:
(
u in I &
v in I )
and A4:
x = [u,v]
by ZFMISC_1:def 2;
reconsider u =
u,
v =
v as
Element of
R by A3;
reconsider u =
u,
v =
v as
Element of
R ;
f . x = u + v
by A1, A2, A4, FUNCT_1:47;
hence
f . x in I
by A3, Def1;
verum
end;
hence
the addF of R || I is BinOp of I
by A1, FUNCT_2:3; verum