let C1, C2 be UnOp of (NonZero F); :: thesis:
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:
for x being object st x in H₁(F) \ {(0. F)} holds
C1 . x = C2 . x

let x be object ; :: thesis:
assume A6: x in H₁(F) \ {(0. F)} ; :: thesis:
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:

end;