let r, h be real-valued Function; :: thesis: ( dom r = dom h & ( for c being set st c in dom r holds
r . c = |.(h . c).| ) implies ( dom r = dom r & ( for c being set st c in dom r holds
r . c = |.(r . c).| ) ) )
assume that
dom r = dom h and
A7: for c being set st c in dom r holds
r . c = |.(h . c).| ; :: thesis: ( dom r = dom r & ( for c being set st c in dom r holds
r . c = |.(r . c).| ) )
thus dom r = dom r ; :: thesis: for c being set st c in dom r holds
r . c = |.(r . c).|
let c be set ; :: thesis: ( c in dom r implies r . c = |.(r . c).| )
assume A8: c in dom r ; :: thesis: r . c = |.(r . c).|
hence r . c = |.|.(h . c).|.| by A7
.= |.(r . c).| by A7, A8 ;
:: thesis: verum