let f, g be UnOp of (setvect M); :: thesis: ( ( for W being Element of setvect M holds W + (f . W) = ID M ) & ( for W being Element of setvect M holds W + (g . W) = ID M ) implies f = g )

assume A3: ( ( for W being Element of setvect M holds W + (f . W) = ID M ) & ( for W being Element of setvect M holds W + (g . W) = ID M ) ) ; :: thesis: f = g

for W being Element of setvect M holds f . W = g . W

assume A3: ( ( for W being Element of setvect M holds W + (f . W) = ID M ) & ( for W being Element of setvect M holds W + (g . W) = ID M ) ) ; :: thesis: f = g

for W being Element of setvect M holds f . W = g . W

proof

hence
f = g
by FUNCT_2:63; :: thesis: verum
let W be Element of setvect M; :: thesis: f . W = g . W

( W + (f . W) = ID M & W + (g . W) = ID M ) by A3;

hence f . W = g . W by Th52; :: thesis: verum

end;( W + (f . W) = ID M & W + (g . W) = ID M ) by A3;

hence f . W = g . W by Th52; :: thesis: verum