let f be Function; :: thesis: for h being Permutation of (dom f) holds dom (f * h) = dom f
let h be Permutation of (dom f); :: thesis: dom (f * h) = dom f
dom (f * h) = h " (dom f) by RELAT_1:147
.= h " (rng h) by FUNCT_2:def 3
.= dom h by RELAT_1:134
.= dom f by FUNCT_2:52 ;
hence dom (f * h) = dom f ; :: thesis: verum