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

proof

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

end;

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

proof

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

end;