defpred S₁[ set , set , set ] means for x1, x2 being VECTOR of X
for y1, y2 being VECTOR of Y st $1 = [x1,y1] & $2 = [x2,y2] holds
$3 = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])];
set A = [: the carrier of X, the carrier of Y:];
A1: for z1, z2 being Element of [: the carrier of X, the carrier of Y:] ex z3 being Element of [: the carrier of X, the carrier of Y:] st S₁[z1,z2,z3]

proof

let z1, z2 be Element of [: the carrier of X, the carrier of Y:]; :: thesis: ex z3 being Element of [: the carrier of X, the carrier of Y:] st S₁[z1,z2,z3]
consider x19, y19 being object such that
A2: x19 in the carrier of X and
A3: y19 in the carrier of Y and
A4: z1 = [x19,y19] by ZFMISC_1:def 2;
consider x29, y29 being object such that
A5: x29 in the carrier of X and
A6: y29 in the carrier of Y and
A7: z2 = [x29,y29] by ZFMISC_1:def 2;
reconsider y19 = y19, y29 = y29 as VECTOR of Y by A3, A6;
reconsider x19 = x19, x29 = x29 as VECTOR of X by A2, A5;
reconsider z3 = [( the addF of X . [x19,x29]),( the addF of Y . [y19,y29])] as Element of [: the carrier of X, the carrier of Y:] ;
take z3 ; :: thesis: S₁[z1,z2,z3]
let x1, x2 be VECTOR of X; :: thesis: for y1, y2 being VECTOR of Y st z1 = [x1,y1] & z2 = [x2,y2] holds
z3 = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])]
let y1, y2 be VECTOR of Y; :: thesis: ( z1 = [x1,y1] & z2 = [x2,y2] implies z3 = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])] )
assume that
A8: z1 = [x1,y1] and
A9: z2 = [x2,y2] ; :: thesis: z3 = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])]
A10: x2 = x29 by A7, A9, XTUPLE_0:1;
A11: y1 = y19 by A4, A8, XTUPLE_0:1;
x1 = x19 by A4, A8, XTUPLE_0:1;
hence z3 = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])] by A7, A9, A10, A11, XTUPLE_0:1; :: thesis: verum

end;

thus ex o being BinOp of [: the carrier of X, the carrier of Y:] st
for a, b being Element of [: the carrier of X, the carrier of Y:] holds S₁[a,b,o . (a,b)] from BINOP_1:sch 3(A1); :: thesis: verum