let m, n be Function; :: thesis: ( ( for x being set holds
( x in dom m iff ex f being Function st
( f in dom F & x = commute f ) ) ) & ( for f being Function st f in dom m holds
m . f = F . (commute f) ) & ( for x being set holds
( x in dom n iff ex f being Function st
( f in dom F & x = commute f ) ) ) & ( for f being Function st f in dom n holds
n . f = F . (commute f) ) implies m = n )
assume that
A7: for x being set holds
( x in dom m iff ex f being Function st
( f in dom F & x = commute f ) ) and
A8: for f being Function st f in dom m holds
m . f = F . (commute f) and
A9: for x being set holds
( x in dom n iff ex f being Function st
( f in dom F & x = commute f ) ) and
A10: for f being Function st f in dom n holds
n . f = F . (commute f) ; :: thesis: m = n

now

let x be set ; :: thesis: ( x in dom m iff x in dom n )
( x in dom m iff ex f being Function st
( f in dom F & x = commute f ) ) by A7;
hence ( x in dom m iff x in dom n ) by A9; :: thesis: verum

end;

then A11: dom m = dom n by TARSKI:2;

now

let x be set ; :: thesis: ( x in dom m implies m . x = n . x )
assume A12: x in dom m ; :: thesis: m . x = n . x
then consider g being Function such that
g in dom F and
A13: x = commute g by A9, A11;
thus m . x = F . (commute (commute g)) by A8, A12, A13
.= n . x by A10, A11, A12, A13 ; :: thesis: verum

end;

hence m = n by A11, FUNCT_1:9; :: thesis: verum