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) )
set g = x .--> f;
A1: dom (x .--> f) = {x} ;
A2: f in Funcs ((dom f),(rng f)) by FUNCT_2:def 2;
rng (x .--> f) = {f} by FUNCOP_1:8;
then rng (x .--> f) c= Funcs ((dom f),(rng f)) by A2, ZFMISC_1:31;
then A3: x .--> f in Funcs ({x},(Funcs ((dom f),(rng f)))) by A1, FUNCT_2:def 2;
A4: (x .--> f) . x = f by FUNCOP_1:72;
A5: x in {x} by TARSKI:def 1;
assume A6: a in dom f ; :: thesis: (commute (x .--> f)) . a = x .--> (f . a)
then A7: ((commute (x .--> f)) . a) . x = f . a by A3, A4, A5, FUNCT_6:56;
dom ((commute (x .--> f)) . a) = {x} by A3, A6, A4, A5, FUNCT_6:56;
hence (commute (x .--> f)) . a = x .--> (f . a) by A7, DICKSON:1; :: thesis: verum