let R be RestFunc; :: thesis: for L being LinearFunc holds
( R (#) L is RestFunc & L (#) R is RestFunc )
let L be LinearFunc; :: thesis: ( R (#) L is RestFunc & L (#) R is RestFunc )
A1: L is total by Def3;
consider x1 being Real such that
A2: for p being Real holds L . p = x1 * p by Def3;
A3: R is total by Def2;

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

let h be non-zero 0 -convergent Real_Sequence; :: thesis: ( (h ") (#) ((R (#) L) /* h) is convergent & lim ((h ") (#) ((R (#) L) /* h)) = 0 )
A5: (h ") (#) (R /* h) is convergent by Def2;

now :: thesis: for n being Element of NAT holds (L /* h) . n = (x1 (#) h) . n

let n be Element of NAT ; :: thesis: (L /* h) . n = (x1 (#) h) . n
thus (L /* h) . n = L . (h . n) by A1, FUNCT_2:115
.= x1 * (h . n) by A2
.= (x1 (#) h) . n by SEQ_1:9 ; :: thesis: verum

end;

then A6: L /* h = x1 (#) h by FUNCT_2:63;
A7: L /* h is convergent by A6;
lim h = 0 ;
then A8: lim (L /* h) = x1 * 0 by A6, SEQ_2:8
.= 0 ;
A9: (h ") (#) ((R (#) L) /* h) = (h ") (#) ((R /* h) (#) (L /* h)) by A3, A1, RFUNCT_2:13
.= ((h ") (#) (R /* h)) (#) (L /* h) by SEQ_1:14 ;
hence (h ") (#) ((R (#) L) /* h) is convergent by A7, A5; :: thesis: lim ((h ") (#) ((R (#) L) /* h)) = 0
lim ((h ") (#) (R /* h)) = 0 by Def2;
hence lim ((h ") (#) ((R (#) L) /* h)) = 0 * 0 by A9, A7, A8, A5, SEQ_2:15
.= 0 ;
:: thesis: verum

end;

hence R (#) L is RestFunc by A3, A1, Def2; :: thesis: L (#) R is RestFunc
thus L (#) R is RestFunc by A3, A1, A4, Def2; :: thesis: verum