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 . b1 = k . b1
per cases ( n = 0 or n > 0 ) ;
suppose n = 0 ; :: thesis: j . b1 = k . b1
hence j . n = k . n by A4, A6; :: thesis: verum
end;
suppose A8: n > 0 ; :: thesis: j . b1 = k . b1
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