let n be Nat; :: thesis: for a, b, c, d being Real holds (rseq (a,b,c,d)) . n = ((a * n) + b) / ((c * n) + d)
let a, b, c, d be Real; :: thesis: (rseq (a,b,c,d)) . n = ((a * n) + b) / ((c * n) + d)
A1: ( dom (Re (Rat_Exp_Seq (a,b,c,d))) = NAT & n in NAT ) by FUNCT_2:def 1, ORDINAL1:def 12;
thus (rseq (a,b,c,d)) . n = Re ((Rat_Exp_Seq (a,b,c,d)) . n) by COMSEQ_3:def 3, A1
.= Re ((Polynom (a,b,n)) / (Polynom (c,d,n))) by Def1
.= Re (((a * n) + b) / (Polynom (c,d,n))) by POLYEQ_1:def 1
.= ((a * n) + b) / ((c * n) + d) by POLYEQ_1:def 1 ; :: thesis: verum