let r be real-valued Function; :: thesis: for b₁ being complex-valued Function st dom r = dom b₁ & ( for c being object st c in dom r holds
r . c = |.(b₁ . c).| ) holds
( dom r = dom r & ( for c being object st c in dom r holds
r . c = |.(r . c).| ) )
let h be complex-valued Function; :: thesis: ( dom r = dom h & ( for c being object st c in dom r holds
r . c = |.(h . c).| ) implies ( dom r = dom r & ( for c being object st c in dom r holds
r . c = |.(r . c).| ) ) )
assume that
dom r = dom h and
A7: for c being object st c in dom r holds
r . c = |.(h . c).| ; :: thesis: ( dom r = dom r & ( for c being object st c in dom r holds
r . c = |.(r . c).| ) )
thus dom r = dom r ; :: thesis: for c being object st c in dom r holds
r . c = |.(r . c).|
let c be object ; :: 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