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
A8: 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 A9: c in dom r ; :: thesis: r . c = |.(r . c).|
hence r . c = |.|.(h . c).|.| by A8
.= |.(r . c).| by A8, A9 ;
:: thesis: verum