A2: dom the addF of V = [: the carrier of V, the carrier of V:] by FUNCT_2:def 1;
A3: for z being object st z in [:V1,V1:] holds
( the addF of V || V1) . z in V1

proof

let z be object ; :: thesis: ( z in [:V1,V1:] implies ( the addF of V || V1) . z in V1 )
assume A4: z in [:V1,V1:] ; :: thesis: ( the addF of V || V1) . z in V1
then consider r, x being object such that
A5: ( r in V1 & x in V1 ) and
A6: z = [r,x] by ZFMISC_1:def 2;
reconsider y = x, r1 = r as Element of V by A5;
[r,x] in dom ( the addF of V || V1) by A2, A4, A6, RELAT_1:62, ZFMISC_1:96;
then ( the addF of V || V1) . z = r1 + y by A6, FUNCT_1:47;
hence ( the addF of V || V1) . z in V1 by A1, A5, IDEAL_1:def 1; :: thesis: verum

end;

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