let seq1, seq2 be sequence of X; :: thesis: ( seq1 . 0 = 1. X & ( for n being Nat holds seq1 . (n + 1) = (seq1 . n) * z ) & seq2 . 0 = 1. X & ( for n being Nat holds seq2 . (n + 1) = (seq2 . n) * z ) implies seq1 = seq2 )

assume that

A4: seq1 . 0 = 1. X and

A5: for n being Nat holds seq1 . (n + 1) = (seq1 . n) * z and

A6: seq2 . 0 = 1. X and

A7: for n being Nat holds seq2 . (n + 1) = (seq2 . n) * z ; :: thesis: seq1 = seq2

defpred S_{1}[ Nat] means seq1 . $1 = seq2 . $1;

A8: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
by A4, A6;

for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A9, A8);

then for n being Element of NAT holds S_{1}[n]
;

hence seq1 = seq2 by FUNCT_2:63; :: thesis: verum

assume that

A4: seq1 . 0 = 1. X and

A5: for n being Nat holds seq1 . (n + 1) = (seq1 . n) * z and

A6: seq2 . 0 = 1. X and

A7: for n being Nat holds seq2 . (n + 1) = (seq2 . n) * z ; :: thesis: seq1 = seq2

defpred S

A8: for k being Nat st S

S

proof

A9:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume S_{1}[k]
; :: thesis: S_{1}[k + 1]

hence seq1 . (k + 1) = (seq2 . k) * z by A5

.= seq2 . (k + 1) by A7 ;

:: thesis: verum

end;assume S

hence seq1 . (k + 1) = (seq2 . k) * z by A5

.= seq2 . (k + 1) by A7 ;

:: thesis: verum

for n being Nat holds S

then for n being Element of NAT holds S

hence seq1 = seq2 by FUNCT_2:63; :: thesis: verum