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_3) + ($2 `1_3)),(($1 `2_3) + ($2 `2_3)),(($1 `3_3) + ($2 `3_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_3) + (y `1_3)),((x `2_3) + (y `2_3)),((x `3_3) + (y `3_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_3) + (y `1_3)),((x `2_3) + (y `2_3)),((x `3_3) + (y `3_3))] by A1; :: thesis: verum