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 set 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 set 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, ZFMISC_1:33;
A11: y1 = y19 by A4, A8, ZFMISC_1:33;
x1 = x19 by A4, A8, ZFMISC_1:33;
hence z3 = [(the addF of X . [x1,x2]),(the addF of Y . [y1,y2])] by A7, A9, A10, A11, ZFMISC_1:33; :: 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