let X, Y be non empty set ; :: thesis: for P being a_partition of Y
for f being Function of X,P st P c= rng f & f is one-to-one holds
f is IndexedPartition of Y
let P be a_partition of Y; :: thesis: for f being Function of X,P st P c= rng f & f is one-to-one holds
f is IndexedPartition of Y
let f be Function of X,P; :: thesis: ( P c= rng f & f is one-to-one implies f is IndexedPartition of Y )
assume P c= rng f ; :: thesis: ( not f is one-to-one or f is IndexedPartition of Y )
then rng f = P ;
hence ( not f is one-to-one or f is IndexedPartition of Y ) by Def2; :: thesis: verum