set f = the carrier of X --> 0;

reconsider f = the carrier of X --> 0 as Function of the carrier of X,REAL by FUNCOP_1:45, XREAL_0:def 1;

reconsider f = f as Functional of X ;

reconsider f = f as linear-Functional of X by Th21X;

f is Lipschitzian by Th21X;

hence ex b_{1} being linear-Functional of X st b_{1} is Lipschitzian
; :: thesis: verum

reconsider f = the carrier of X --> 0 as Function of the carrier of X,REAL by FUNCOP_1:45, XREAL_0:def 1;

reconsider f = f as Functional of X ;

reconsider f = f as linear-Functional of X by Th21X;

f is Lipschitzian by Th21X;

hence ex b