let m, n be Function; :: thesis: ( ( for x being object 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 object 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
A8: for x being object holds
( x in dom m iff ex f being Function st
( f in dom F & x = commute f ) ) and
A9: for f being Function st f in dom m holds
m . f = F . (commute f) and
A10: for x being object holds
( x in dom n iff ex f being Function st
( f in dom F & x = commute f ) ) and
A11: for f being Function st f in dom n holds
n . f = F . (commute f) ; :: thesis: m = n

now :: thesis: for x being object holds
( x in dom m iff x in dom n )

let x be object ; :: 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 A8;
hence ( x in dom m iff x in dom n ) by A10; :: thesis: verum

end;

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

now :: thesis: for x being object st x in dom m holds
m . x = n . x

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

end;

hence m = n by A12, FUNCT_1:2; :: thesis: verum