let f1, f2 be UnOp of [.0,1.]; :: thesis: ( ( 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 ) ) ; :: thesis: f1 = f2
for x being Element of [.0,1.] holds f1 . x = f2 . x

proof

let x be Element of [.0,1.]; :: thesis: f1 . x = f2 . x

per cases ( x = 1 or x <> 1 ) ;

suppose D1: x = 1 ; :: thesis: f1 . x = f2 . x

hence f1 . x = 0 by A1
.= f2 . x by D1, A2 ;
:: thesis: verum

end;

suppose D1: x <> 1 ; :: thesis: f1 . x = f2 . x

hence f1 . x = 1 by A1
.= f2 . x by D1, A2 ;
:: thesis: verum

end;

end;

end;

hence f1 = f2 by FUNCT_2:63; :: thesis: verum