let r, 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 h = dom r & ( for c being object st c in dom h holds
h . c = (r . c) " ) ) )
assume that
A7: dom r = dom h and
A8: for c being object st c in dom r holds
r . c = (h . c) " ; :: thesis: ( dom h = dom r & ( for c being object st c in dom h holds
h . c = (r . c) " ) )
thus dom r = dom h by A7; :: thesis: for c being object st c in dom h holds
h . c = (r . c) "
let c be object ; :: thesis: ( c in dom h implies h . c = (r . c) " )
assume A9: c in dom h ; :: thesis: h . c = (r . c) "
thus h . c = ((h . c) ") "
.= (r . c) " by A7, A8, A9 ; :: thesis: verum