let Omega be non empty finite set ; :: thesis: for f being PartFunc of Omega,REAL holds dom (f * (canFS (dom f))) = dom (canFS (dom f))
let f be PartFunc of Omega,REAL; :: thesis: dom (f * (canFS (dom f))) = dom (canFS (dom f))
rng (canFS (dom f)) c= dom f ;
hence dom (f * (canFS (dom f))) = dom (canFS (dom f)) by RELAT_1:27; :: thesis: verum