let x, a be set ; :: thesis: for f being Function st a in dom f holds
(commute (x .--> f)) . a = x .--> (f . a)
let f be Function; :: thesis: ( a in dom f implies (commute (x .--> f)) . a = x .--> (f . a) )
assume A1: a in dom f ; :: thesis: (commute (x .--> f)) . a = x .--> (f . a)
set g = x .--> f;
A2: ( dom (x .--> f) = {x} & rng (x .--> f) = {f} & (x .--> f) . x = f ) by FUNCOP_1:14, FUNCOP_1:19, FUNCOP_1:87;
A3: x in {x} by TARSKI:def 1;
f in Funcs (dom f),(rng f) by FUNCT_2:def 2;
then rng (x .--> f) c= Funcs (dom f),(rng f) by A2, ZFMISC_1:37;
then x .--> f in Funcs {x},(Funcs (dom f),(rng f)) by A2, FUNCT_2:def 2;
then ( dom ((commute (x .--> f)) . a) = {x} & ((commute (x .--> f)) . a) . x = f . a ) by A1, A2, A3, FUNCT_6:86;
hence (commute (x .--> f)) . a = x .--> (f . a) by DICKSON:1; :: thesis: verum