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
proof
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;
hence f = g by FUNCT_2:63; :: thesis: verum