let rseq1, rseq2 be Real_Sequence; :: thesis: ( rseq1 . 0 = 1 & ( for n being Nat holds rseq1 . (n + 1) = (rseq1 . n) * (n + 1) ) & rseq2 . 0 = 1 & ( for n being Nat holds rseq2 . (n + 1) = (rseq2 . n) * (n + 1) ) implies rseq1 = rseq2 )
assume that
A3: rseq1 . 0 = 1 and
A4: for n being Nat holds rseq1 . (n + 1) = (rseq1 . n) * (n + 1) and
A5: rseq2 . 0 = 1 and
A6: for n being Nat holds rseq2 . (n + 1) = (rseq2 . n) * (n + 1) ; :: thesis: rseq1 = rseq2
defpred S₁[ Nat] means rseq1 . $1 = rseq2 . $1;
A7: S₁[ 0 ] by A3, A5;
A8: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume rseq1 . k = rseq2 . k ; :: thesis: S₁[k + 1]
hence rseq1 . (k + 1) = (rseq2 . k) * (k + 1) by A4
.= rseq2 . (k + 1) by A6 ;
:: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A7, A8);
hence rseq1 = rseq2 ; :: thesis: verum