defpred S1[ 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 S1[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 S1[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: S1[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 ;
A11: y1 = y19 by ;
x1 = x19 by ;
hence z3 = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])] by ; :: 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 S1[a,b,o . (a,b)] from :: thesis: verum