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