let f1, f2 be UnOp of E; ( ( for b being Point of E holds f1 . b = (2 * a) - b ) & ( for b being Point of E holds f2 . b = (2 * a) - b ) implies f1 = f2 )
assume that
A1:
for b being Point of E holds f1 . b = (2 * a) - b
and
A2:
for b being Point of E holds f2 . b = (2 * a) - b
; f1 = f2
let b be Point of E; FUNCT_2:def 8 f1 . b = f2 . b
thus f1 . b =
(2 * a) - b
by A1
.=
f2 . b
by A2
; verum