let i be Element of NAT ; :: thesis: for f being PartFunc of (REAL i),REAL holds dom (<>* f) = dom f
let f be PartFunc of (REAL i),REAL; :: thesis: dom (<>* f) = dom f
rng f c= dom ((proj (1,1)) ") by PDIFF_1:2;
hence dom (<>* f) = dom f by RELAT_1:27; :: thesis: verum