let L1, L2 be LINEAR; :: thesis: L1 (#) L2 is REST-like
consider x1 being Real such that
A1: for p being Real holds L1 . p = x1 * p by Def4;
A2: ( L1 is total & L2 is total ) by Def4;
hence L1 (#) L2 is total ; :: according to FDIFF_1:def 3 :: thesis: for h being convergent_to_0 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 Def4;

now

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

now

let n be Element of NAT ; :: thesis: ((h " ) (#) ((L1 (#) L2) /* h)) . n = ((x1 * x2) (#) h) . n
h is non-zero by Def1;
then A4: h . n <> 0 by SEQ_1:7;
thus ((h " ) (#) ((L1 (#) L2) /* h)) . n = ((h " ) . n) * (((L1 (#) L2) /* h) . n) by SEQ_1:12
.= ((h " ) . n) * ((L1 (#) L2) . (h . n)) by A2, FUNCT_2:192
.= ((h " ) . n) * ((L1 . (h . n)) * (L2 . (h . n))) by A2, RFUNCT_1:72
.= (((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:13 ; :: thesis: verum

end;

then A5: (h " ) (#) ((L1 (#) L2) /* h) = (x1 * x2) (#) h by FUNCT_2:113;
A6: h is convergent by Def1;
hence (h " ) (#) ((L1 (#) L2) /* h) is convergent by A5, SEQ_2:21; :: thesis: lim ((h " ) (#) ((L1 (#) L2) /* h)) = 0
lim h = 0 by Def1;
hence lim ((h " ) (#) ((L1 (#) L2) /* h)) = (x1 * x2) * 0 by A6, A5, SEQ_2:22
.= 0 ;
:: thesis: verum

end;

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