deffunc H₁( set ) -> Element of NAT = 0 ;
deffunc H₂( Real) -> set = (2 * $1) - 1;
defpred S₁[ Real] means $1 <= 1 / 2;
consider f being Function such that
A1: ( dom f = the carrier of I[01] & ( for x being Element of I[01] holds
( ( S₁[x] implies f . x = H₁(x) ) & ( not S₁[x] implies f . x = H₂(x) ) ) ) ) from PARTFUN1:sch 4();
for x being object st x in the carrier of I[01] holds
f . x in the carrier of I[01]

proof

let x be object ; :: thesis: ( x in the carrier of I[01] implies f . x in the carrier of I[01] )
assume x in the carrier of I[01] ; :: thesis: f . x in the carrier of I[01]
then reconsider x = x as Point of I[01] ;

per cases ( S₁[x] or not S₁[x] ) ;

suppose S₁[x] ; :: thesis: f . x in the carrier of I[01]

then f . x = 0 by A1;
hence f . x in the carrier of I[01] by BORSUK_1:43; :: thesis: verum

end;

suppose A2: not S₁[x] ; :: thesis: f . x in the carrier of I[01]

then f . x = H₂(x) by A1;
then f . x is Point of I[01] by A2, Th4;
hence f . x in the carrier of I[01] ; :: thesis: verum

end;

end;

end;

then reconsider f = f as Function of I[01],I[01] by A1, FUNCT_2:3;
for t being Point of I[01] holds
( ( t <= 1 / 2 implies f . t = 0 ) & ( t > 1 / 2 implies f . t = (2 * t) - 1 ) ) by A1;
hence ex b₁ being Function of I[01],I[01] st
for t being Point of I[01] holds
( ( t <= 1 / 2 implies b₁ . t = 0 ) & ( t > 1 / 2 implies b₁ . t = (2 * t) - 1 ) ) ; :: thesis: verum