reconsider f = the addF 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 A2:
x in [:I,I:]
;
:: thesis: f . x in I
then consider u,
v being
set such that A3:
(
u in I &
v in I &
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, A3, FUNCT_1:70;
hence
f . x in I
by A3, Def1;
:: thesis: verum
end;
hence
the addF of R || I is BinOp of I
by A1, FUNCT_2:5; :: thesis: verum