let X be set ; :: thesis: for P being non-empty Function st Union P = X & ( for x, y being set st x in dom P & y in dom P & x <> y holds
P . x misses P . y ) holds
P is IndexedPartition of X
let P be non-empty Function; :: thesis: ( Union P = X & ( for x, y being set st x in dom P & y in dom P & x <> y holds
P . x misses P . y ) implies P is IndexedPartition of X )
assume that
A1: Union P = X and
A2: for x, y being set st x in dom P & y in dom P & x <> y holds
P . x misses P . y ; :: thesis: P is IndexedPartition of X
rng P c= bool X

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng P or y in bool X )
assume y in rng P ; :: thesis: y in bool X
then y c= union (rng P) by ZFMISC_1:92;
then y c= X by A1, CARD_3:def 4;
hence y in bool X ; :: thesis: verum

end;

then reconsider Y = rng P as Subset-Family of X ;
Y is a_partition of X

proof

thus union Y = X by A1, CARD_3:def 4; :: according to EQREL_1:def 6 :: thesis: for b₁ being Element of bool X holds
( not b₁ in Y or ( not b₁ = {} & ( for b₂ being Element of bool X holds
( not b₂ in Y or b₁ = b₂ or b₁ misses b₂ ) ) ) )
let A be Subset of X; :: thesis: ( not A in Y or ( not A = {} & ( for b₁ being Element of bool X holds
( not b₁ in Y or A = b₁ or A misses b₁ ) ) ) )
assume A in Y ; :: thesis: ( not A = {} & ( for b₁ being Element of bool X holds
( not b₁ in Y or A = b₁ or A misses b₁ ) ) )
then A3: ex x being set st
( x in dom P & A = P . x ) by FUNCT_1:def 5;
hence A <> {} by FUNCT_1:def 15; :: thesis: for b₁ being Element of bool X holds
( not b₁ in Y or A = b₁ or A misses b₁ )
let B be Subset of X; :: thesis: ( not B in Y or A = B or A misses B )
assume B in Y ; :: thesis: ( A = B or A misses B )
then ex y being set st
( y in dom P & B = P . y ) by FUNCT_1:def 5;
hence ( A = B or A misses B ) by A2, A3; :: thesis: verum

end;

hence rng P is a_partition of X ; :: according to PUA2MSS1:def 3 :: thesis: P is one-to-one
let x, y be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x in dom P or not y in dom P or not P . x = P . y or x = y )
assume A4: ( x in dom P & y in dom P & P . x = P . y & x <> y ) ; :: thesis: contradiction
then reconsider Px = P . x, Py = P . y as non empty set by FUNCT_1:def 15;
consider a being Element of Px;
P . x misses P . y by A2, A4;
then not a in Py by XBOOLE_0:3;
hence contradiction by A4; :: thesis: verum