let f1, f2 be Function of I[01],I[01]; ( ( 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 ) )
; f1 = f2
for t being Point of I[01] holds f1 . t = f2 . t
hence
f1 = f2
by FUNCT_2:63; verum