let f, g be BinOp of H1(F); ( ( 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))]
; 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)
hence
f = g
by BINOP_1:2; verum