defpred S₁[ object ] means $1 = 1;
deffunc H₁( object ) -> Element of NAT = 0 ;
deffunc H₂( object ) -> Element of NAT = 1;
A1: for x being object st x in [.0,1.] holds
( ( S₁[x] implies H₁(x) in [.0,1.] ) & ( not S₁[x] implies H₂(x) in [.0,1.] ) ) by XXREAL_1:1;
ex f being Function of [.0,1.],[.0,1.] st
for x being object st x in [.0,1.] holds
( ( S₁[x] implies f . x = H₁(x) ) & ( not S₁[x] implies f . x = H₂(x) ) ) from FUNCT_2:sch 5(A1);
then consider f being Function of [.0,1.],[.0,1.] such that
B1: for x being object st x in [.0,1.] holds
( ( S₁[x] implies f . x = H₁(x) ) & ( not S₁[x] implies f . x = H₂(x) ) ) ;
take f ; :: thesis: for x being Element of [.0,1.] holds
( ( x = 1 implies f . x = 0 ) & ( x <> 1 implies f . x = 1 ) )
let x be Element of [.0,1.]; :: thesis: ( ( x = 1 implies f . x = 0 ) & ( x <> 1 implies f . x = 1 ) )
thus ( x = 1 implies f . x = 0 ) by B1; :: thesis: ( x <> 1 implies f . x = 1 )
assume x <> 1 ; :: thesis: f . x = 1
hence f . x = 1 by B1; :: thesis: verum