deffunc H₂( Element of H₁(F), Element of H₁(F)) -> Element of [: the carrier of F, the carrier of F, the carrier of F:] = [(($1 `1) + ($2 `1)),(($1 `2) + ($2 `2)),(($1 `3) + ($2 `3))];
consider f being BinOp of H₁(F) such that
A1: for x, y being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds f . (x,y) = H₂(x,y) from BINOP_1:sch 4();
take f ; :: thesis: for x, y being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds f . (x,y) = [((x `1) + (y `1)),((x `2) + (y `2)),((x `3) + (y `3))]
thus for x, y being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds f . (x,y) = [((x `1) + (y `1)),((x `2) + (y `2)),((x `3) + (y `3))] by A1; :: thesis: verum