set f = the carrier of X --> (0. Y);

reconsider f = the carrier of X --> (0. Y) as LinearOperator of X,Y by Th18;

take f ; :: thesis: f is Lipschitzian

for x being VECTOR of X holds f . x = 0. Y by FUNCOP_1:7;

hence f is Lipschitzian by Th20; :: thesis: verum

reconsider f = the carrier of X --> (0. Y) as LinearOperator of X,Y by Th18;

take f ; :: thesis: f is Lipschitzian

for x being VECTOR of X holds f . x = 0. Y by FUNCOP_1:7;

hence f is Lipschitzian by Th20; :: thesis: verum