let F be Function; :: thesis: ( dom F = {{}} implies Commute F = F )
assume A1: dom F = {{}} ; :: thesis: Commute F = F
A2: dom (Commute F) = {{}}

proof

thus dom (Commute F) c= {{}} :: according to XBOOLE_0:def 10 :: thesis: {{}} c= dom (Commute F)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (Commute F) or x in {{}} )
assume x in dom (Commute F) ; :: thesis: x in {{}}
then ex f being Function st
( f in dom F & x = commute f ) by Def1;
then x = {} by A1, FUNCT_6:58, TARSKI:def 1;
hence x in {{}} by TARSKI:def 1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {{}} or x in dom (Commute F) )
assume x in {{}} ; :: thesis: x in dom (Commute F)
then A3: x = {} by TARSKI:def 1;
{} in dom F by A1, TARSKI:def 1;
hence x in dom (Commute F) by A3, Def1, FUNCT_6:58; :: thesis: verum

end;

for x being object st x in {{}} holds
(Commute F) . x = F . x

proof

let x be object ; :: thesis: ( x in {{}} implies (Commute F) . x = F . x )
assume A4: x in {{}} ; :: thesis: (Commute F) . x = F . x
then x = {} by TARSKI:def 1;
hence (Commute F) . x = F . x by A2, A4, Def1, FUNCT_6:58; :: thesis: verum

end;

hence Commute F = F by A1, A2, FUNCT_1:2; :: thesis: verum