let j, k be Real_Sequence; :: thesis: ( j . 0 = 0 & ( for n being Element of NAT st n > 0 holds
j . n = n to_power a ) & k . 0 = 0 & ( for n being Element of NAT st n > 0 holds
k . n = n to_power a ) implies j = k )
assume that
A3: ( j . 0 = 0 & ( for n being Element of NAT st n > 0 holds
j . n = n to_power a ) ) and
A4: ( k . 0 = 0 & ( for n being Element of NAT st n > 0 holds
k . n = n to_power a ) ) ; :: thesis: j = k

now

let n be Element of NAT ; :: thesis: j . b₁ = k . b₁

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

suppose n = 0 ; :: thesis: j . b₁ = k . b₁

hence j . n = k . n by A3, A4; :: thesis: verum

end;

suppose A5: n > 0 ; :: thesis: j . b₁ = k . b₁

then j . n = n to_power a by A3;
hence j . n = k . n by A4, A5; :: thesis: verum

end;

end;

end;

hence j = k by FUNCT_2:113; :: thesis: verum