let m, n be Function; :: thesis:
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:

let x be object ; :: thesis:
( 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:

end;

let x be object ; :: thesis:
assume A13: x in dom m ; :: thesis:
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:

end;