let f1, f2 be Function of I[01],I[01]; :: thesis: ( ( for t being Point of I[01] holds
( ( t <= 1 / 2 implies f1 . t = 2 * t ) & ( t > 1 / 2 implies f1 . t = 1 ) ) ) & ( for t being Point of I[01] holds
( ( t <= 1 / 2 implies f2 . t = 2 * t ) & ( t > 1 / 2 implies f2 . t = 1 ) ) ) implies f1 = f2 )
assume that
A3: for t being Point of I[01] holds
( ( t <= 1 / 2 implies f1 . t = 2 * t ) & ( t > 1 / 2 implies f1 . t = 1 ) ) and
A4: for t being Point of I[01] holds
( ( t <= 1 / 2 implies f2 . t = 2 * t ) & ( t > 1 / 2 implies f2 . t = 1 ) ) ; :: thesis: f1 = f2
for t being Point of I[01] holds f1 . t = f2 . t

proof

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

per cases ( t <= 1 / 2 or t > 1 / 2 ) ;

suppose A5: t <= 1 / 2 ; :: thesis: f1 . t = f2 . t

then f1 . t = 2 * t by A3
.= f2 . t by A4, A5 ;
hence f1 . t = f2 . t ; :: thesis: verum

end;

suppose A6: t > 1 / 2 ; :: thesis: f1 . t = f2 . t

then f1 . t = 1 by A3
.= f2 . t by A4, A6 ;
hence f1 . t = f2 . t ; :: thesis: verum

end;

end;

end;

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