let L1, L2 be LINEAR; :: thesis: L1 (#) L2 is REST-like
A1: L1 is total by Def4;
A2: L2 is total by Def4;
hence L1 (#) L2 is total by A1; :: 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 x1 being Real such that
A4: for p being Real holds L1 . p = x1 * p by Def4;
consider x2 being Real such that
A5: 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 )
A6: ( h is convergent & lim h = 0 ) by Def1;

now

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

end;

then A8: (h " ) (#) ((L1 (#) L2) /* h) = (x1 * x2) (#) h by FUNCT_2:113;
hence (h " ) (#) ((L1 (#) L2) /* h) is convergent by A6, SEQ_2:21; :: thesis: lim ((h " ) (#) ((L1 (#) L2) /* h)) = 0
thus lim ((h " ) (#) ((L1 (#) L2) /* h)) = (x1 * x2) * 0 by A6, A8, 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