let s1, s2 be Complex_Sequence; ( s1 . 0 = s . 0 & ( for n being Nat holds s1 . (n + 1) = (s1 . n) * (s . (n + 1)) ) & s2 . 0 = s . 0 & ( for n being Nat holds s2 . (n + 1) = (s2 . n) * (s . (n + 1)) ) implies s1 = s2 )
assume A1:
( s1 . 0 = s . 0 & ( for n being Nat holds s1 . (n + 1) = (s1 . n) * (s . (n + 1)) ) & s2 . 0 = s . 0 & ( for n being Nat holds s2 . (n + 1) = (s2 . n) * (s . (n + 1)) ) )
; s1 = s2
for n being Element of NAT holds s1 . n = s2 . n
proof
defpred S1[
Nat]
means s1 . $1
= s2 . $1;
B1:
S1[
0 ]
by A1;
B2:
for
n being
Nat st
S1[
n] holds
S1[
n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume
s1 . n = s2 . n
;
S1[n + 1]
then s1 . (n + 1) =
(s2 . n) * (s . (n + 1))
by A1
.=
s2 . (n + 1)
by A1
;
hence
S1[
n + 1]
;
verum
end;
for
n being
Nat holds
S1[
n]
from NAT_1:sch 2(B1, B2);
hence
for
n being
Element of
NAT holds
s1 . n = s2 . n
;
verum
end;
hence
s1 = s2
by FUNCT_2:63; verum