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 object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng P or y in bool X )
reconsider yy = y as set by TARSKI:1;
assume y in rng P ; :: thesis: y in bool X
then yy c= union (rng P) by ZFMISC_1:74;
then yy 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 4 :: 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 A3: 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 A4: ex x being object st
( x in dom P & A = P . x ) by FUNCT_1:def 3;
thus A <> {} by A3; :: 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 object st
( y in dom P & B = P . y ) by FUNCT_1:def 3;
hence ( A = B or A misses B ) by A2, A4; :: thesis: verum

end;

hence rng P is a_partition of X ; :: according to PUA2MSS1:def 2 :: thesis: P is one-to-one
let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in proj1 P or not y in proj1 P or not P . x = P . y or x = y )
assume that
A5: x in dom P and
A6: y in dom P and
A7: P . x = P . y and
A8: x <> y ; :: thesis: contradiction
reconsider Px = P . x, Py = P . y as non empty set by A5, A6, FUNCT_1:def 9;
set a = the Element of Px;
P . x misses P . y by A2, A5, A6, A8;
then not the Element of Px in Py by XBOOLE_0:3;
hence contradiction by A7; :: thesis: verum