let f1, f2 be UnOp of E; :: thesis: ( ( 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 ; :: thesis: f1 = f2
let b be Point of E; :: according to FUNCT_2:def 8 :: thesis: f1 . b = f2 . b
thus f1 . b = (2 * a) - b by A1
.= f2 . b by A2 ; :: thesis: verum