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

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

A3: for z being object st z in [:X1,X1:] holds

( the addF of X || X1) . z in X1

proof

dom ( the addF of X || X1) = [:X1,X1:]
by A2, RELAT_1:62, ZFMISC_1:96;
let z be object ; :: 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 object such that

A5: ( r in X1 & x in X1 ) and

A6: 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, A6, RELAT_1:62, ZFMISC_1:96;

then ( the addF of X || X1) . z = r1 + y by A6, FUNCT_1:47;

hence ( the addF of X || X1) . z in X1 by A1, A5; :: thesis: verum

end;assume A4: z in [:X1,X1:] ; :: thesis: ( the addF of X || X1) . z in X1

consider r, x being object such that

A5: ( r in X1 & x in X1 ) and

A6: 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, A6, RELAT_1:62, ZFMISC_1:96;

then ( the addF of X || X1) . z = r1 + y by A6, FUNCT_1:47;

hence ( the addF of X || X1) . z in X1 by A1, A5; :: thesis: verum

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