A1: dom the addF of X = [: the carrier of X, the carrier of X:] by FUNCT_2:def 1;
A2: for z being set st z in [:X1,X1:] holds
( the addF of X || X1) . z in X1

proof

let z be set ; :: thesis: ( z in [:X1,X1:] implies ( the addF of X || X1) . z in X1 )
assume A3: z in [:X1,X1:] ; :: thesis: ( the addF of X || X1) . z in X1
consider r, x being set such that
A4: ( r in X1 & x in X1 ) and
A5: z = [r,x] by A3, ZFMISC_1:def 2;
reconsider y = x, r1 = r as VECTOR of X by A4;
[r,x] in dom ( the addF of X || X1) by A1, A3, A5, RELAT_1:62, ZFMISC_1:96;
then ( the addF of X || X1) . z = r1 + y by A5, FUNCT_1:47;
hence ( the addF of X || X1) . z in X1 by B1, A4, RLSUB_1:def 1; :: thesis: verum

end;

dom ( the addF of X || X1) = [:X1,X1:] by A1, RELAT_1:62, ZFMISC_1:96;
hence the addF of X || X1 is BinOp of X1 by A2, FUNCT_2:3; :: thesis: verum