let C1, C2 be UnOp of (NonZero F); :: thesis: ( ( for x being Element of NonZero F holds (omf F) . (x,(C1 . x)) = 1. F ) & ( for x being Element of NonZero F holds (omf F) . (x,(C2 . x)) = 1. F ) implies C1 = C2 )
assume that
A4: for x being Element of NonZero F holds (omf F) . (x,(C1 . x)) = 1. F and
A5: for x being Element of NonZero F holds (omf F) . (x,(C2 . x)) = 1. F ; :: thesis: C1 = C2
for x being object st x in H₁(F) \ {(0. F)} holds
C1 . x = C2 . x

proof

let x be object ; :: thesis: ( x in H₁(F) \ {(0. F)} implies C1 . x = C2 . x )
assume A6: x in H₁(F) \ {(0. F)} ; :: thesis: C1 . x = C2 . x
then A7: C1 . x is Element of NonZero F by FUNCT_2:5;
then reconsider a = x, C1a = C1 . x as Element of F by A6;
A8: C2 . x is Element of NonZero F by A6, FUNCT_2:5;
then reconsider C2a = C2 . x as Element of F ;
C1 . x = C1a * (1. F)
.= C1a * (a * C2a) by A5, A6
.= (a * C1a) * C2a by A6, A7, A8, Th4
.= (1. F) * C2a by A4, A6
.= C2 . x ;
hence C1 . x = C2 . x ; :: thesis: verum

end;

hence C1 = C2 by FUNCT_2:12; :: thesis: verum