let a, c, d be Real; ( 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))
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 ;
FUNCT_2:def 8 (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
;
verum
end;
thus
rseq (a,0,c,d) = (- a) (#) (rseq (1,0,(- c),(- d)))
verumproof
set f =
rseq (
a,
0,
c,
d);
set f1 =
rseq (1,
0,
(- c),
(- d));
let n be
Element of
NAT ;
FUNCT_2:def 8 (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
;
verum
end;