let f be Membership_Func of REAL; :: thesis: f is bounded
ex r being Real st
for x being set st x in dom f holds
|.(f . x).| < r

proof

take 1 + 1 ; :: thesis: for x being set st x in dom f holds
|.(f . x).| < 1 + 1
thus for x being set st x in dom f holds
|.(f . x).| < 1 + 1 :: thesis: verum

proof

let x be set ; :: thesis: ( x in dom f implies |.(f . x).| < 1 + 1 )
assume x in dom f ; :: thesis: |.(f . x).| < 1 + 1
then reconsider x = x as Element of REAL ;
f . x = |.(f . x).| by FUZZY_2:1, COMPLEX1:43;
then |.(f . x).| + 0 < 1 + 1 by XREAL_1:8, FUZZY_2:1;
hence |.(f . x).| < 1 + 1 ; :: thesis: verum

end;

end;

hence f is bounded by COMSEQ_2:def 3; :: thesis: verum