defpred S₁[ set , set , set ] means for x1, x2 being VECTOR of
for y1, y2 being VECTOR of 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 x1', y1' being set such that
A2: x1' in the carrier of X and
A3: y1' in the carrier of Y and
A4: z1 = [x1',y1'] by ZFMISC_1:def 2;
consider x2', y2' being set such that
A5: x2' in the carrier of X and
A6: y2' in the carrier of Y and
A7: z2 = [x2',y2'] by ZFMISC_1:def 2;
reconsider y1' = y1', y2' = y2' as VECTOR of by A3, A6;
reconsider x1' = x1', x2' = x2' as VECTOR of by A2, A5;
reconsider z3 = [(the addF of X . [x1',x2']),(the addF of Y . [y1',y2'])] as Element of [:the carrier of X,the carrier of Y:] ;
take z3 ; :: thesis: S₁[z1,z2,z3]
let x1, x2 be VECTOR of ; :: thesis: for y1, y2 being VECTOR of 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 ; :: 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 = x2' by A7, A9, ZFMISC_1:33;
A11: y1 = y1' by A4, A8, ZFMISC_1:33;
x1 = x1' 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