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