now :: thesis: for h being non-zero 0 -convergent Complex_Sequence holds
( (h ") (#) ((R1 (#) R2) /* h) is convergent & lim ((h ") (#) ((R1 (#) R2) /* h)) = 0c )
let h be non-zero 0 -convergent Complex_Sequence; :: thesis: ( (h ") (#) ((R1 (#) R2) /* h) is convergent & lim ((h ") (#) ((R1 (#) R2) /* h)) = 0c )
for seq being Complex_Sequence st seq is non-zero holds
seq " is non-zero
proof
let seq be Complex_Sequence; :: thesis: ( seq is non-zero implies seq " is non-zero )
assume that
A6: seq is non-zero and
A7: not seq " is non-zero ; :: thesis: contradiction
consider n1 being Element of NAT such that
A8: (seq ") . n1 = 0c by A7, COMSEQ_1:4;
(seq . n1) " = (seq ") . n1 by VALUED_1:10;
hence contradiction by A6, A8, COMSEQ_1:4, XCMPLX_1:202; :: thesis: verum
end;
then A9: h " is non-zero ;
A10: (h ") (#) ((R1 (#) R2) /* h) = ((R1 /* h) (#) (R2 /* h)) /" h by CFCONT_1:14
.= (((R1 /* h) (#) (R2 /* h)) (#) (h ")) /" (h (#) (h ")) by A9, COMSEQ_1:37
.= (((R1 /* h) (#) (R2 /* h)) (#) (h ")) (#) (((h ") ") (#) (h ")) by COMSEQ_1:30
.= (h (#) (h ")) (#) ((R1 /* h) (#) ((h ") (#) (R2 /* h))) by COMSEQ_1:8
.= ((h (#) (h ")) (#) (R1 /* h)) (#) ((h ") (#) (R2 /* h)) by COMSEQ_1:8
.= (h (#) ((h ") (#) (R1 /* h))) (#) ((h ") (#) (R2 /* h)) by COMSEQ_1:8 ;
A11: (h ") (#) (R1 /* h) is convergent by Def3;
then A12: h (#) ((h ") (#) (R1 /* h)) is convergent ;
( lim ((h ") (#) (R1 /* h)) = 0c & lim h = 0c ) by Def1, Def3;
then A13: lim (h (#) ((h ") (#) (R1 /* h))) = 0 * 0 by A11, COMSEQ_2:30
.= 0c ;
A14: (h ") (#) (R2 /* h) is convergent by Def3;
hence (h ") (#) ((R1 (#) R2) /* h) is convergent by A12, A10; :: thesis: lim ((h ") (#) ((R1 (#) R2) /* h)) = 0c
lim ((h ") (#) (R2 /* h)) = 0c by Def3;
hence lim ((h ") (#) ((R1 (#) R2) /* h)) = 0c * 0c by A14, A12, A13, A10, COMSEQ_2:30
.= 0c ;
:: thesis: verum
end;
hence for b1 being PartFunc of COMPLEX,COMPLEX st b1 = R1 (#) R2 holds
( b1 is total & b1 is RestFunc-like ) ; :: thesis: verum