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