let f1, f2 be UnOp of [.0,1.]; ( ( for x being Element of [.0,1.] holds
( ( x = 1 implies f1 . x = 0 ) & ( x <> 1 implies f1 . x = 1 ) ) ) & ( for x being Element of [.0,1.] holds
( ( x = 1 implies f2 . x = 0 ) & ( x <> 1 implies f2 . x = 1 ) ) ) implies f1 = f2 )
assume that
A1:
for x being Element of [.0,1.] holds
( ( x = 1 implies f1 . x = 0 ) & ( x <> 1 implies f1 . x = 1 ) )
and
A2:
for x being Element of [.0,1.] holds
( ( x = 1 implies f2 . x = 0 ) & ( x <> 1 implies f2 . x = 1 ) )
; f1 = f2
for x being Element of [.0,1.] holds f1 . x = f2 . x
hence
f1 = f2
by FUNCT_2:63; verum