let b, c, d be Real; :: thesis: ( rseq (0,b,c,d) = b (#) (rseq (0,1,c,d)) & rseq (0,b,c,d) = (- b) (#) (rseq (0,1,(- c),(- d))) )
thus rseq (0,b,c,d) = b (#) (rseq (0,1,c,d)) :: thesis: rseq (0,b,c,d) = (- b) (#) (rseq (0,1,(- c),(- d)))

proof

set f1 = rseq (0,1,c,d);
let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: (rseq (0,b,c,d)) . n = (b (#) (rseq (0,1,c,d))) . n
thus (rseq (0,b,c,d)) . n = ((0 * n) + b) / ((c * n) + d) by Th5
.= b * (((0 * n) + 1) / ((c * n) + d))
.= b * ((rseq (0,1,c,d)) . n) by Th5
.= (b (#) (rseq (0,1,c,d))) . n by VALUED_1:6 ; :: thesis: verum

end;

thus rseq (0,b,c,d) = (- b) (#) (rseq (0,1,(- c),(- d))) :: thesis: verum

proof

set f1 = rseq (0,1,(- c),(- d));
let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: (rseq (0,b,c,d)) . n = ((- b) (#) (rseq (0,1,(- c),(- d)))) . n
thus (rseq (0,b,c,d)) . n = ((0 * n) + b) / ((c * n) + d) by Th5
.= ((- 1) * b) / ((- 1) * ((c * n) + d)) by XCMPLX_1:91
.= (- b) * (((0 * n) + 1) / (((- c) * n) + (- d)))
.= (- b) * ((rseq (0,1,(- c),(- d))) . n) by Th5
.= ((- b) (#) (rseq (0,1,(- c),(- d)))) . n by VALUED_1:6 ; :: thesis: verum

end;