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
||.((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, the carrier of S 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
||.(((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
||.(((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 ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| <= s * (abs (x1 - x2)) )
assume A4: ( x1 in dom (p (#) f) & x2 in dom (p (#) f) ) ; :: thesis: ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| <= s * (abs (x1 - x2))
A6: 0 <= abs (x1 - x2) by COMPLEX1:132;
||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| = ||.((p * (f /. x1)) - ((p (#) f) /. x2)).|| by A4, VFUNCT_1:def 4
.= ||.((p * (f /. x1)) - (p * (f /. x2))).|| by A4, VFUNCT_1:def 4
.= ||.((0. S) - (p * (f /. x2))).|| by A3, RLVECT_1:23
.= ||.((0. S) - (0. S)).|| by A3, RLVECT_1:23
.= 0 by NORMSP_1:10 ;
hence ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| <= s * (abs (x1 - x2)) by A1, A6; :: thesis: verum

end;

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

end;

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

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

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
||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| <= g * (abs (x1 - x2)) ) )
A8: 0 <= abs p by COMPLEX1:132;
thus 0 < g by A7; :: thesis: for x1, x2 being real number st x1 in dom (p (#) f) & x2 in dom (p (#) f) holds
||.(((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 ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| <= g * (abs (x1 - x2)) )
assume A9: ( x1 in dom (p (#) f) & x2 in dom (p (#) f) ) ; :: thesis: ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| <= g * (abs (x1 - x2))
then A11: ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| = ||.((p * (f /. x1)) - ((p (#) f) /. x2)).|| by VFUNCT_1:def 4
.= ||.((p * (f /. x1)) - (p * (f /. x2))).|| by A9, VFUNCT_1:def 4
.= ||.(p * ((f /. x1) - (f /. x2))).|| by RLVECT_1:48
.= (abs p) * ||.((f /. x1) - (f /. x2)).|| by NORMSP_1:def 2 ;
( x1 in dom f & x2 in dom f ) by A9, VFUNCT_1:def 4;
then (abs p) * ||.((f /. x1) - (f /. x2)).|| <= (abs p) * (s * (abs (x1 - x2))) by A2, A8, XREAL_1:66;
hence ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| <= g * (abs (x1 - x2)) by A11; :: thesis: verum

end;

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

end;

end;