consider s being real number such that
A1: 0 < s and
A2: for x1, x2 being real number st x1 in dom f & x2 in dom f holds
abs ((f . x1) - (f . x2)) <= s * (abs (x1 - x2)) by Def3;

per cases ( p = 0 or p <> 0 ) ;

suppose A3: p = 0 ; :: thesis: for b₁ being PartFunc of REAL,REAL st b₁ = p (#) f holds
b₁ is Lipschitzian

now

take s = s; :: thesis: ( 0 < s & ( for x1, x2 being real number st x1 in dom (p (#) f) & x2 in dom (p (#) f) holds
abs (((p (#) f) . x1) - ((p (#) f) . x2)) <= s * (abs (x1 - x2)) ) )
thus 0 < s by A1; :: thesis: for x1, x2 being real number st x1 in dom (p (#) f) & x2 in dom (p (#) f) holds
abs (((p (#) f) . x1) - ((p (#) f) . x2)) <= s * (abs (x1 - x2))
let x1, x2 be real number ; :: thesis: ( x1 in dom (p (#) f) & x2 in dom (p (#) f) implies abs (((p (#) f) . x1) - ((p (#) f) . x2)) <= s * (abs (x1 - x2)) )
assume that
A4: x1 in dom (p (#) f) and
A5: x2 in dom (p (#) f) ; :: thesis: abs (((p (#) f) . x1) - ((p (#) f) . x2)) <= s * (abs (x1 - x2))
A6: 0 <= abs (x1 - x2) by COMPLEX1:46;
abs (((p (#) f) . x1) - ((p (#) f) . x2)) = abs ((p * (f . x1)) - ((p (#) f) . x2)) by A4, VALUED_1:def 5
.= abs (0 - (p * (f . x2))) by A3, A5, VALUED_1:def 5
.= 0 by A3, ABSVALUE:2 ;
hence abs (((p (#) f) . x1) - ((p (#) f) . x2)) <= s * (abs (x1 - x2)) by A1, A6; :: thesis: verum

end;

hence for b₁ being PartFunc of REAL,REAL st b₁ = p (#) f holds
b₁ is Lipschitzian by Def3; :: thesis: verum

end;

suppose p <> 0 ; :: thesis: for b₁ being PartFunc of REAL,REAL st b₁ = p (#) f holds
b₁ is Lipschitzian

then 0 < abs p by COMPLEX1:47;
then A7: 0 * s < (abs p) * s by A1, XREAL_1:68;

now

take g = (abs p) * s; :: thesis: ( 0 < g & ( for x1, x2 being real number st x1 in dom (p (#) f) & x2 in dom (p (#) f) holds
abs (((p (#) f) . x1) - ((p (#) f) . x2)) <= g * (abs (x1 - x2)) ) )
A8: 0 <= abs p by COMPLEX1:46;
thus 0 < g by A7; :: thesis: for x1, x2 being real number st x1 in dom (p (#) f) & x2 in dom (p (#) f) holds
abs (((p (#) f) . x1) - ((p (#) f) . x2)) <= g * (abs (x1 - x2))
let x1, x2 be real number ; :: thesis: ( x1 in dom (p (#) f) & x2 in dom (p (#) f) implies abs (((p (#) f) . x1) - ((p (#) f) . x2)) <= g * (abs (x1 - x2)) )
assume that
A9: x1 in dom (p (#) f) and
A10: x2 in dom (p (#) f) ; :: thesis: abs (((p (#) f) . x1) - ((p (#) f) . x2)) <= g * (abs (x1 - x2))
A11: abs (((p (#) f) . x1) - ((p (#) f) . x2)) = abs ((p * (f . x1)) - ((p (#) f) . x2)) by A9, VALUED_1:def 5
.= abs ((p * (f . x1)) - (p * (f . x2))) by A10, VALUED_1:def 5
.= abs (p * ((f . x1) - (f . x2)))
.= (abs p) * (abs ((f . x1) - (f . x2))) by COMPLEX1:65 ;
( x1 in dom f & x2 in dom f ) by A9, A10, VALUED_1:def 5;
then (abs p) * (abs ((f . x1) - (f . x2))) <= (abs p) * (s * (abs (x1 - x2))) by A2, A8, XREAL_1:64;
hence abs (((p (#) f) . x1) - ((p (#) f) . x2)) <= g * (abs (x1 - x2)) by A11; :: thesis: verum

end;

hence for b₁ being PartFunc of REAL,REAL st b₁ = p (#) f holds
b₁ is Lipschitzian by Def3; :: thesis: verum

end;

end;