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

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