let f, g be BinOp of H₁(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))] ) & ( for x, y being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds g . (x,y) = [((x `1_3) + (y `1_3)),((x `2_3) + (y `2_3)),((x `3_3) + (y `3_3))] ) implies f = g )
assume that
A2: 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))] and
A3: for x, y being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds g . (x,y) = [((x `1_3) + (y `1_3)),((x `2_3) + (y `2_3)),((x `3_3) + (y `3_3))] ; :: thesis: f = g
for x, y being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds f . (x,y) = g . (x,y)

proof

let x, y be Element of [: the carrier of F, the carrier of F, the carrier of F:]; :: thesis: f . (x,y) = g . (x,y)
thus f . (x,y) = [((x `1_3) + (y `1_3)),((x `2_3) + (y `2_3)),((x `3_3) + (y `3_3))] by A2
.= g . (x,y) by A3 ; :: thesis: verum

end;

hence f = g by BINOP_1:2; :: thesis: verum