let r be Real; :: thesis: for f being PartFunc of REAL,REAL st f = REAL --> r holds
f | REAL is continuous
let f be PartFunc of REAL,REAL; :: thesis: ( f = REAL --> r implies f | REAL is continuous )
assume A1: f = REAL --> r ; :: thesis: f | REAL is continuous
f | REAL is constant
proof
reconsider r = r as Element of REAL by XREAL_0:def 1;
take r ; :: according to PARTFUN2:def 1 :: thesis: for b1 being Element of REAL holds
( not b1 in dom (f | REAL) or (f | REAL) . b1 = r )
let c be Element of REAL ; :: thesis: ( not c in dom (f | REAL) or (f | REAL) . c = r )
assume c in dom (f | REAL) ; :: thesis: (f | REAL) . c = r
thus (f | REAL) . c = f . c
.= r by A1, FUNCOP_1:7 ; :: thesis: verum
end;
hence f | REAL is continuous ; :: thesis: verum