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 that
A3: for W being Element of setvect M holds W + (f . W) = ID M and
A4: 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
A5: W + (f . W) = ID M by A3;
W + (g . W) = ID M by A4;
hence f . W = g . W by A5, Th78; :: thesis: verum

end;

hence f = g by FUNCT_2:113; :: thesis: verum