consider b1 being Complex such that
A1: for z being Complex holds L /. z = b1 * z by Def4;

now :: thesis: for h being non-zero 0 -convergent Complex_Sequence holds
( (h ") (#) ((R (#) L) /* h) is convergent & lim ((h ") (#) ((R (#) L) /* h)) = 0c )

let h be non-zero 0 -convergent Complex_Sequence; :: thesis: ( (h ") (#) ((R (#) L) /* h) is convergent & lim ((h ") (#) ((R (#) L) /* h)) = 0c )
A2: (h ") (#) ((R (#) L) /* h) = (h ") (#) ((R /* h) (#) (L /* h)) by CFCONT_1:14
.= ((h ") (#) (R /* h)) (#) (L /* h) by COMSEQ_1:8 ;

now :: thesis: for n being Element of NAT holds (L /* h) . n = (b1 (#) h) . n

let n be Element of NAT ; :: thesis: (L /* h) . n = (b1 (#) h) . n
thus (L /* h) . n = L /. (h . n) by FUNCT_2:115
.= b1 * (h . n) by A1
.= (b1 (#) h) . n by VALUED_1:6 ; :: thesis: verum

end;

then A3: L /* h = b1 (#) h ;
lim h = 0c by Def1;
then A4: lim (L /* h) = b1 * 0c by A3, COMSEQ_2:18
.= 0c ;
A5: (h ") (#) (R /* h) is convergent by Def3;
hence (h ") (#) ((R (#) L) /* h) is convergent by A2, A3; :: thesis: lim ((h ") (#) ((R (#) L) /* h)) = 0c
lim ((h ") (#) (R /* h)) = 0c by Def3;
hence lim ((h ") (#) ((R (#) L) /* h)) = 0c * 0c by A2, A3, A4, A5, COMSEQ_2:30
.= 0c ;
:: thesis: verum

end;

hence for b₁ being PartFunc of COMPLEX,COMPLEX st b₁ = R (#) L holds
( b₁ is total & b₁ is RestFunc-like ) ; :: thesis: verum