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) + (y `1)),((x `2) + (y `2)),((x `3) + (y `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) + (y `1)),((x `2) + (y `2)),((x `3) + (y `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) + (y `1)),((x `2) + (y `2)),((x `3) + (y `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) + (y `1)),((x `2) + (y `2)),((x `3) + (y `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) + (y `1)),((x `2) + (y `2)),((x `3) + (y `3))] by A2
.= g . (x,y) by A3 ; :: thesis: verum

end;

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