let f1, f2 be Real_Sequence; :: thesis: ( f1 . 0 = 0 & ( for k being non zero Nat holds f1 . k = (a . k) / (b to_power (k !)) ) & f2 . 0 = 0 & ( for k being non zero Nat holds f2 . k = (a . k) / (b to_power (k !)) ) implies f1 = f2 )
assume that
A1: ( f1 . 0 = 0 & ( for n being non zero Nat holds f1 . n = (a . n) / (b to_power (n !)) ) ) and
A2: ( f2 . 0 = 0 & ( for n being non zero Nat holds f2 . n = (a . n) / (b to_power (n !)) ) ) ; :: 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 A1, A2; :: thesis: verum

end;

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

then f1 . n = (a . n) / (b to_power (n !)) by A1
.= f2 . n by A2, A3 ;
hence f1 . n = f2 . n ; :: thesis: verum

end;

end;

end;

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