let f1, f2 be Real_Sequence; :: thesis: ( f1 . 0 = 0 & ( for i being non zero Nat holds f1 . i = 1 / (TSqF i) ) & f2 . 0 = 0 & ( for i being non zero Nat holds f2 . i = 1 / (TSqF i) ) implies f1 = f2 )
assume that
A1: ( f1 . 0 = 0 & ( for i being non zero Nat holds f1 . i = 1 / (TSqF i) ) ) and
A2: ( f2 . 0 = 0 & ( for i being non zero Nat holds f2 . i = 1 / (TSqF i) ) ) ; :: thesis: f1 = f2
for n being Element of NAT holds f1 . n = f2 . n

proof

let n be Element of NAT ; :: thesis: f1 . n = f2 . n

per cases ( n = 0 or n <> 0 ) ;

suppose n = 0 ; :: thesis: f1 . n = f2 . n

hence f1 . n = f2 . n by A2, A1; :: thesis: verum

end;

suppose n <> 0 ; :: thesis: f1 . n = f2 . n

then reconsider nn = n as non zero Nat ;
f1 . nn = 1 / (TSqF nn) by A1
.= f2 . nn by A2 ;
hence f1 . n = f2 . n ; :: thesis: verum

end;

end;

end;

hence f1 = f2 by FUNCT_2:63; :: thesis: verum