let L1, L2 be LinearFunc; :: thesis:
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:
consider x2 being Real such that
A3: for p being Real holds L2 . p = x2 * p by Def3;

let n be Element of NAT ; :: thesis:
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:

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 = 0 ;
hence lim ((h ") (#) ((L1 (#) L2) /* h)) = (x1 * x2) * 0 by A5, SEQ_2:8
.= 0 ;
:: thesis:

end;