let L1, L2 be LinearFunc; :: thesis: L1 (#) L2 is RestFunc-like
consider x1 being Real such that
A1: for p being Real holds L1 . p = x1 * p by Def3;
A2: ( L1 is total & L2 is total ) by Def3;
hence L1 (#) L2 is total ; :: according to FDIFF_1:def 2 :: thesis: for h being non-zero 0 -convergent Real_Sequence holds
( (h ") (#) ((L1 (#) L2) /* h) is convergent & lim ((h ") (#) ((L1 (#) L2) /* h)) = 0 )
consider x2 being Real such that
A3: for p being Real holds L2 . p = x2 * p by Def3;

now :: thesis: for h being non-zero 0 -convergent Real_Sequence holds
( (h ") (#) ((L1 (#) L2) /* h) is convergent & lim ((h ") (#) ((L1 (#) L2) /* h)) = 0 )

let h be non-zero 0 -convergent Real_Sequence; :: thesis: ( (h ") (#) ((L1 (#) L2) /* h) is convergent & lim ((h ") (#) ((L1 (#) L2) /* h)) = 0 )

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

let n be Element of NAT ; :: thesis: ((h ") (#) ((L1 (#) L2) /* h)) . n = ((x1 * x2) (#) h) . n
A4: h . n <> 0 by SEQ_1:5;
thus ((h ") (#) ((L1 (#) L2) /* h)) . n = ((h ") . n) * (((L1 (#) L2) /* h) . n) by SEQ_1:8
.= ((h ") . n) * ((L1 (#) L2) . (h . n)) by A2, FUNCT_2:115
.= ((h ") . n) * ((L1 . (h . n)) * (L2 . (h . n))) by A2, RFUNCT_1:56
.= (((h ") . n) * (L1 . (h . n))) * (L2 . (h . n))
.= (((h . n) ") * (L1 . (h . n))) * (L2 . (h . n)) by VALUED_1:10
.= (((h . n) ") * ((h . n) * x1)) * (L2 . (h . n)) by A1
.= ((((h . n) ") * (h . n)) * x1) * (L2 . (h . n))
.= (1 * x1) * (L2 . (h . n)) by A4, XCMPLX_0:def 7
.= x1 * (x2 * (h . n)) by A3
.= (x1 * x2) * (h . n)
.= ((x1 * x2) (#) h) . n by SEQ_1:9 ; :: thesis: verum

end;

then A5: (h ") (#) ((L1 (#) L2) /* h) = (x1 * x2) (#) h by FUNCT_2:63;
thus (h ") (#) ((L1 (#) L2) /* h) is convergent by A5; :: thesis: lim ((h ") (#) ((L1 (#) L2) /* h)) = 0
lim h = 0 ;
hence lim ((h ") (#) ((L1 (#) L2) /* h)) = (x1 * x2) * 0 by A5, SEQ_2:8
.= 0 ;
:: thesis: verum

end;

hence for h being non-zero 0 -convergent Real_Sequence holds
( (h ") (#) ((L1 (#) L2) /* h) is convergent & lim ((h ") (#) ((L1 (#) L2) /* h)) = 0 ) ; :: thesis: verum