let j, k be Real_Sequence; :: thesis: ( j . 0 = 0 & ( for n being Element of NAT st n > 0 holds
j . n = log (2,n) ) & k . 0 = 0 & ( for n being Element of NAT st n > 0 holds
k . n = log (2,n) ) implies j = k )
assume that
A4: j . 0 = 0 and
A5: for n being Element of NAT st n > 0 holds
j . n = log (2,n) and
A6: k . 0 = 0 and
A7: for n being Element of NAT st n > 0 holds
k . n = log (2,n) ; :: thesis: j = k

now :: thesis: for n being Element of NAT holds j . n = k . n

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 A4, A6; :: thesis: verum

end;

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

then j . n = log (2,n) by A5;
hence j . n = k . n by A7, A8; :: thesis: verum

end;

end;

end;

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