let f be Function; :: thesis: for x being object st x in dom f holds
(commute <*f*>) . x = <*(f . x)*>
let x be object ; :: thesis: ( x in dom f implies (commute <*f*>) . x = <*(f . x)*> )
assume A1: x in dom f ; :: thesis: (commute <*f*>) . x = <*(f . x)*>
thus (commute <*f*>) . x = (commute {[1,f]}) . x by FINSEQ_1:def 5
.= (commute (1 .--> f)) . x by FUNCT_4:82
.= 1 .--> (f . x) by A1, TOPGEN_5:3
.= {[1,(f . x)]} by FUNCT_4:82
.= <*(f . x)*> by FINSEQ_1:def 5 ; :: thesis: verum