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;

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

( 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 )

hence
R (#) L is RestFunc
by A3, A1, Def2; :: thesis: L (#) R is RestFunc( (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;

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;A5: (h ") (#) (R /* h) is convergent by Def2;

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

then A6:
L /* h = x1 (#) h
by FUNCT_2:63;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;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

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

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