let F1, F2 be real-valued Function; :: thesis: ( dom F1 = dom f & ( for x being object st x in dom f holds
F1 . x = r to_power (f . x) ) & dom F2 = dom f & ( for x being object st x in dom f holds
F2 . x = r to_power (f . x) ) implies F1 = F2 )
assume that
A3: ( dom F1 = dom f & ( for x being object st x in dom f holds
F1 . x = r to_power (f . x) ) ) and
A4: ( dom F2 = dom f & ( for x being object st x in dom f holds
F2 . x = r to_power (f . x) ) ) ; :: thesis: F1 = F2

now :: thesis: for x being object st x in dom f holds
F1 . x = F2 . x

let x be object ; :: thesis: ( x in dom f implies F1 . x = F2 . x )
assume A5: x in dom f ; :: thesis: F1 . x = F2 . x
hence F1 . x = r to_power (f . x) by A3
.= F2 . x by A4, A5 ;
:: thesis: verum

end;

hence F1 = F2 by A3, A4; :: thesis: verum