let P be IndexedPartition of X; :: thesis: ( P is one-to-one & P is non-empty )
thus P is one-to-one by Def2; :: thesis: P is non-empty
let x be object ; :: according to FUNCT_1:def 9 :: thesis: ( not x in proj1 P or not P . x is empty )
assume x in dom P ; :: thesis: not P . x is empty
then P . x in rng P by FUNCT_1:def 3;
hence not P . x is empty ; :: thesis: verum