A2:
dom the addF of X = [: the carrier of X, the carrier of X:]
by FUNCT_2:def 1;
A3:
for z being object st z in [:X1,X1:] holds
( the addF of X || X1) . z in X1
proof
let z be
object ;
( z in [:X1,X1:] implies ( the addF of X || X1) . z in X1 )
assume A4:
z in [:X1,X1:]
;
( the addF of X || X1) . z in X1
consider r,
x being
object such that A5:
r in X1
and A6:
x in X1
and A7:
z = [r,x]
by A4, ZFMISC_1:def 2;
reconsider y =
x,
r1 =
r as
VECTOR of
X by A5, A6;
[r,x] in dom ( the addF of X || X1)
by A2, A4, A7, RELAT_1:62, ZFMISC_1:96;
then
( the addF of X || X1) . z = r1 + y
by A7, FUNCT_1:47;
hence
( the addF of X || X1) . z in X1
by A1, A5, A6;
verum
end;
dom ( the addF of X || X1) = [:X1,X1:]
by A2, RELAT_1:62, ZFMISC_1:96;
hence
the addF of X || X1 is BinOp of X1
by A3, FUNCT_2:3; verum