reconsider LL = L1 (#) L2 as PartFunc of COMPLEX,COMPLEX ;
LL is RestFunc-like

proof

let h be non-zero 0 -convergent Complex_Sequence; :: according to CFDIFF_1:def 3 :: thesis: ( (h ") (#) (LL /* h) is convergent & lim ((h ") (#) (LL /* h)) = 0 )
consider b1 being Complex such that
A1: for z being Complex holds L1 /. z = b1 * z by Def4;
consider b2 being Complex such that
A2: for z being Complex holds L2 /. z = b2 * z by Def4;

A3: now :: thesis: for n being Element of NAT holds ((h ") (#) ((L1 (#) L2) /* h)) . n = ((b1 * b2) (#) h) . n

let n be Element of NAT ; :: thesis: ((h ") (#) ((L1 (#) L2) /* h)) . n = ((b1 * b2) (#) h) . n
A4: h . n <> 0c by COMSEQ_1:4;
thus ((h ") (#) ((L1 (#) L2) /* h)) . n = ((h ") . n) * (((L1 (#) L2) /* h) . n) by VALUED_1:5
.= ((h ") . n) * ((L1 (#) L2) /. (h . n)) by FUNCT_2:115
.= ((h ") . n) * ((L1 /. (h . n)) * (L2 /. (h . n))) by CFUNCT_1:64
.= (((h ") . n) * (L1 /. (h . n))) * (L2 /. (h . n))
.= (((h . n) ") * (L1 /. (h . n))) * (L2 /. (h . n)) by VALUED_1:10
.= (((h . n) ") * ((h . n) * b1)) * (L2 /. (h . n)) by A1
.= ((((h . n) ") * (h . n)) * b1) * (L2 /. (h . n))
.= (1r * b1) * (L2 /. (h . n)) by A4, XCMPLX_0:def 7
.= b1 * (b2 * (h . n)) by A2
.= (b1 * b2) * (h . n)
.= ((b1 * b2) (#) h) . n by VALUED_1:6 ; :: thesis: verum

end;

then A5: (h ") (#) ((L1 (#) L2) /* h) = (b1 * b2) (#) h ;
thus (h ") (#) (LL /* h) is convergent by A3, FUNCT_2:63; :: thesis: lim ((h ") (#) (LL /* h)) = 0
lim h = 0c by Def1;
hence lim ((h ") (#) (LL /* h)) = (b1 * b2) * 0c by A5, COMSEQ_2:18
.= 0c ;
:: thesis: verum

end;

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