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
A3: j . 0 = 0 and
A4: for n being Element of NAT st n > 0 holds
j . n = log (2,n) and
A5: k . 0 = 0 and
A6: for n being Element of NAT st n > 0 holds
k . n = log (2,n) ; :: 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, A5; :: thesis: verum

end;

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

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

end;

end;

end;

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