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

A4: now

let h be convergent_to_0 Real_Sequence; :: thesis: ( (h ") (#) ((R (#) L) /* h) is convergent & lim ((h ") (#) ((R (#) L) /* h)) = 0 )
A5: (h ") (#) (R /* h) is convergent by Def3;

now

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: h is convergent by Def1;
then A8: L /* h is convergent by A6, SEQ_2:7;
lim h = 0 by Def1;
then A9: lim (L /* h) = x1 * 0 by A7, A6, SEQ_2:8
.= 0 ;
A10: (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 A8, A5, SEQ_2:14; :: thesis: lim ((h ") (#) ((R (#) L) /* h)) = 0
lim ((h ") (#) (R /* h)) = 0 by Def3;
hence lim ((h ") (#) ((R (#) L) /* h)) = 0 * 0 by A10, A8, A9, A5, SEQ_2:15
.= 0 ;
:: thesis: verum

end;

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