let f be bijective decreasing UnOp of [.0,1.]; ( f . 0 = 1 & f . 1 = 0 )
KK:
f . 0 = 1
proof
set y =
f . 0;
set X =
[.0,1.];
K1:
1
in [.0,1.]
by XXREAL_1:1;
reconsider y =
f . 0 as
Element of
[.0,1.] by XXREAL_1:1, FUNCT_2:5;
assume H0:
f . 0 <> 1
;
contradiction
I3:
rng f = [.0,1.]
by FUNCT_2:def 3;
reconsider z =
(f ") . 1 as
Element of
[.0,1.] by XXREAL_1:1, FUNCT_2:5;
L1:
f . z = 1
by FUNCT_1:35, I3, K1;
then consider zz being
Element of
[.0,1.] such that L2:
zz < z
by Wazne1, H0;
f . zz > f . z
by L2, Decreas;
hence
contradiction
by L1, XXREAL_1:1;
verum
end;
f . 1 = 0
proof
set X =
[.0,1.];
K1:
0 in [.0,1.]
by XXREAL_1:1;
reconsider y =
f . 1 as
Element of
[.0,1.] by XXREAL_1:1, FUNCT_2:5;
assume H0:
f . 1
<> 0
;
contradiction
I3:
rng f = [.0,1.]
by FUNCT_2:def 3;
reconsider z =
(f ") . 0 as
Element of
[.0,1.] by XXREAL_1:1, FUNCT_2:5;
L1:
f . z = 0
by FUNCT_1:35, I3, K1;
then consider zz being
Element of
[.0,1.] such that L2:
zz > z
by Wazne2, H0;
f . zz < f . z
by L2, Decreas;
hence
contradiction
by L1, XXREAL_1:1;
verum
end;
hence
( f . 0 = 1 & f . 1 = 0 )
by KK; verum