deffunc H₁( real number ) -> Element of REAL = (2 * $1) - 1;
deffunc H₂( real number ) -> Element of REAL = $1 - (1 / 4);
deffunc H₃( real number ) -> Element of REAL = (1 / 2) * $1;
defpred S₁[ real number ] means $1 > 3 / 4;
defpred S₂[ real number ] means ( $1 > 1 / 2 & $1 <= 3 / 4 );
defpred S₃[ real number ] means $1 <= 1 / 2;
A1: for c being Element of holds
( S₃[c] or S₂[c] or S₁[c] ) ;
A2: for c being Element of holds
( ( S₃[c] implies not S₂[c] ) & ( S₃[c] implies not S₁[c] ) & ( S₂[c] implies not S₁[c] ) ) by XXREAL_0:2;
consider f being Function such that
A3: ( dom f = the carrier of I[01] & ( for c being Element of holds
( ( S₃[c] implies f . c = H₃(c) ) & ( S₂[c] implies f . c = H₂(c) ) & ( S₁[c] implies f . c = H₁(c) ) ) ) ) from BORSUK_6:sch 1(A2, A1);
for x being set st x in the carrier of I[01] holds
f . x in the carrier of I[01]

proof

let x be set ; :: 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 ;

per cases ( S₃[x] or S₂[x] or S₁[x] ) ;

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

then f . x = (1 / 2) * x by A3;
then f . x is Point of by Th9;
hence f . x in the carrier of I[01] ; :: thesis: verum

end;

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

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

end;

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

then f . x = (2 * x) - 1 by A3;
then f . x is Point of by A5, Th7, XXREAL_0:2;
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 A3, FUNCT_2:5;
for x being Point of holds
( ( x <= 1 / 2 implies f . x = (1 / 2) * x ) & ( x > 1 / 2 & x <= 3 / 4 implies f . x = x - (1 / 4) ) & ( x > 3 / 4 implies f . x = (2 * x) - 1 ) ) by A3;
hence ex b₁ being Function of I[01] ,I[01] st
for x being Point of holds
( ( x <= 1 / 2 implies b₁ . x = (1 / 2) * x ) & ( x > 1 / 2 & x <= 3 / 4 implies b₁ . x = x - (1 / 4) ) & ( x > 3 / 4 implies b₁ . x = (2 * x) - 1 ) ) ; :: thesis: verum