defpred S_{1}[ 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_{1}[z1,z2,z3]

for a, b being Element of [: the carrier of X, the carrier of Y:] holds S_{1}[a,b,o . (a,b)]
from BINOP_1:sch 3(A1); :: thesis: verum

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

proof

thus
ex o being BinOp of [: the carrier of X, the carrier of Y:] st
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_{1}[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_{1}[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;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

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

for a, b being Element of [: the carrier of X, the carrier of Y:] holds S