A2: dom the addF of X = [:the carrier of X,the carrier of X:] by FUNCT_2:def 1;
then A3: dom (the addF of X || X1) = [:X1,X1:] by RELAT_1:91, ZFMISC_1:119;
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 A4: z in [:X1,X1:] ; :: thesis: (the addF of X || X1) . z in X1
consider r, x being set such that
A5: ( r in X1 & x in X1 & z = [r,x] ) by A4, ZFMISC_1:def 2;
reconsider y = x, r1 = r as VECTOR of X by A5;
[r,x] in dom (the addF of X || X1) by A2, A4, A5, RELAT_1:91, ZFMISC_1:119;
then (the addF of X || X1) . z = r1 + y by A5, FUNCT_1:70;
hence (the addF of X || X1) . z in X1 by A1, A5, CLVECT_1:def 4; :: thesis: verum

end;

hence the addF of X || X1 is BinOp of X1 by A3, FUNCT_2:5; :: thesis: verum