let c1, c2 be Complex; :: thesis: for g being complex-valued Function holds (g (/) c1) (#) c2 = (g (#) c2) (/) c1
let g be complex-valued Function; :: thesis: (g (/) c1) (#) c2 = (g (#) c2) (/) c1
A1: dom ((g (/) c1) (#) c2) = dom (g (/) c1) by VALUED_1:def 5;
( dom (g (/) c1) = dom g & dom (g (#) c2) = dom g ) by VALUED_1:def 5;
hence dom ((g (/) c1) (#) c2) = dom ((g (#) c2) (/) c1) by ; :: according to FUNCT_1:def 11 :: thesis: for b1 being object holds
( not b1 in dom ((g (/) c1) (#) c2) or ((g (/) c1) (#) c2) . b1 = ((g (#) c2) (/) c1) . b1 )

let x be object ; :: thesis: ( not x in dom ((g (/) c1) (#) c2) or ((g (/) c1) (#) c2) . x = ((g (#) c2) (/) c1) . x )
assume x in dom ((g (/) c1) (#) c2) ; :: thesis: ((g (/) c1) (#) c2) . x = ((g (#) c2) (/) c1) . x
thus ((g (/) c1) (#) c2) . x = ((g (/) c1) . x) * c2 by VALUED_1:6
.= ((g . x) * (c1 ")) * c2 by VALUED_1:6
.= ((g . x) * c2) * (c1 ")
.= ((g (#) c2) . x) * (c1 ") by VALUED_1:6
.= ((g (#) c2) (/) c1) . x by VALUED_1:6 ; :: thesis: verum