set f = REAL --> (0* n);
A1: [#] REAL = dom (REAL --> (0* n)) by FUNCT_2:def 1;
now :: thesis: for x being Real st x in [#] REAL holds
(REAL --> (0* n)) /. x = (x * (0* n)) + (0* n)
let x be Real; :: thesis: ( x in [#] REAL implies (REAL --> (0* n)) /. x = (x * (0* n)) + (0* n) )
assume x in [#] REAL ; :: thesis: (REAL --> (0* n)) /. x = (x * (0* n)) + (0* n)
reconsider xx = x as Element of REAL by XREAL_0:def 1;
A2: (REAL --> (0* n)) /. xx = 0* n by FUNCOP_1:7
.= 0. (TOP-REAL n) by EUCLID:70
.= x * (0. (TOP-REAL n)) by RLVECT_1:10
.= (x * (0. (TOP-REAL n))) + (0. (TOP-REAL n)) by RLVECT_1:4 ;
A3: x * (0. (TOP-REAL n)) = x (#) (0* n) by EUCLID:65, EUCLID:70;
0. (TOP-REAL n) = 0* n by EUCLID:70;
hence (REAL --> (0* n)) /. x = (x * (0* n)) + (0* n) by A2, A3, EUCLID:64; :: thesis: verum
end;
then REAL --> (0* n) is_differentiable_on [#] REAL by A1, Th18;
hence for b1 being Function of REAL,(REAL n) st b1 = REAL --> (0* n) holds
b1 is differentiable by A1; :: thesis: verum