deffunc H₁( Real) -> set = (2 * $1) - 1;
deffunc H₂( Real) -> set = $1 - (1 / 4);
deffunc H₃( Real) -> set = (1 / 2) * $1;
defpred S₁[ Real] means $1 > 3 / 4;
defpred S₂[ Real] means ( $1 > 1 / 2 & $1 <= 3 / 4 );
defpred S₃[ Real] means $1 <= 1 / 2;
A1: for c being Element of I[01] holds
( S₃[c] or S₂[c] or S₁[c] ) ;
A2: for c being Element of I[01] 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 I[01] 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 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 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 I[01] by Th6;
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 I[01] by A4, Th7;
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 I[01] by A5, Th4, 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:3;
for x being Point of I[01] 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 I[01] 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