set f = REAL --> (0* n);

A1: [#] REAL = dom (REAL --> (0* n)) by FUNCT_2:def 1;

hence for b_{1} being Function of REAL,(REAL n) st b_{1} = REAL --> (0* n) holds

b_{1} is differentiable
by A1; :: thesis: verum

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)

then
REAL --> (0* n) is_differentiable_on [#] REAL
by A1, Th18;(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;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

hence for b

b