:: deftheorem Def1 defines Commute PRALG_2:def 1 :
for F, b₂ being Function holds
( b₂ = Commute F iff ( ( for x being object holds
( x in dom b₂ iff ex f being Function st
( f in dom F & x = commute f ) ) ) & ( for f being Function st f in dom b₂ holds
b₂ . f = F . (commute f) ) ) );