let f1, f2 be Function of I[01],I[01]; :: thesis: ( ( for x being Point of I[01] holds
( ( x <= 1 / 2 implies f1 . x = (1 / 2) * x ) & ( x > 1 / 2 & x <= 3 / 4 implies f1 . x = x - (1 / 4) ) & ( x > 3 / 4 implies f1 . x = (2 * x) - 1 ) ) ) & ( for x being Point of I[01] holds
( ( x <= 1 / 2 implies f2 . x = (1 / 2) * x ) & ( x > 1 / 2 & x <= 3 / 4 implies f2 . x = x - (1 / 4) ) & ( x > 3 / 4 implies f2 . x = (2 * x) - 1 ) ) ) implies f1 = f2 )
assume that
A6: for x being Point of I[01] holds
( ( x <= 1 / 2 implies f1 . x = (1 / 2) * x ) & ( x > 1 / 2 & x <= 3 / 4 implies f1 . x = x - (1 / 4) ) & ( x > 3 / 4 implies f1 . x = (2 * x) - 1 ) ) and
A7: for x being Point of I[01] holds
( ( x <= 1 / 2 implies f2 . x = (1 / 2) * x ) & ( x > 1 / 2 & x <= 3 / 4 implies f2 . x = x - (1 / 4) ) & ( x > 3 / 4 implies f2 . x = (2 * x) - 1 ) ) ; :: thesis: f1 = f2
for x being Point of I[01] holds f1 . x = f2 . x

proof

let x be Point of I[01]; :: thesis: f1 . x = f2 . x

per cases ( x <= 1 / 2 or ( x > 1 / 2 & x <= 3 / 4 ) or x > 3 / 4 ) ;

suppose A8: x <= 1 / 2 ; :: thesis: f1 . x = f2 . x

then f1 . x = (1 / 2) * x by A6
.= f2 . x by A7, A8 ;
hence f1 . x = f2 . x ; :: thesis: verum

end;

suppose A9: ( x > 1 / 2 & x <= 3 / 4 ) ; :: thesis: f1 . x = f2 . x

then f1 . x = x - (1 / 4) by A6
.= f2 . x by A7, A9 ;
hence f1 . x = f2 . x ; :: thesis: verum

end;

suppose A10: x > 3 / 4 ; :: thesis: f1 . x = f2 . x

then f1 . x = (2 * x) - 1 by A6
.= f2 . x by A7, A10 ;
hence f1 . x = f2 . x ; :: thesis: verum

end;

end;

end;

hence f1 = f2 by FUNCT_2:63; :: thesis: verum