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 set ; :: 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 consider f being Function such that
A3: ( f in dom F & x = commute f ) by Def6;
x = {} by A1, A3, FUNCT_6:88, TARSKI:def 1;
hence x in {{} } by TARSKI:def 1; :: thesis: verum

end;

let x be set ; :: 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 A4: x = {} by TARSKI:def 1;
{} in dom F by A1, TARSKI:def 1;
hence x in dom (Commute F) by A4, Def6, FUNCT_6:88; :: thesis: verum

end;

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

proof

let x be set ; :: thesis: ( x in {{} } implies (Commute F) . x = F . x )
assume A5: x in {{} } ; :: thesis: (Commute F) . x = F . x
then x = {} by TARSKI:def 1;
hence (Commute F) . x = F . x by A2, A5, Def6, FUNCT_6:88; :: thesis: verum

end;

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