let X be set ; :: thesis: for Y being non empty set
for f being Function of X,Y holds { (f " {y}) where y is Element of Y : y in rng f } is a_partition of X
let Y be non empty set ; :: thesis: for f being Function of X,Y holds { (f " {y}) where y is Element of Y : y in rng f } is a_partition of X
let f be Function of X,Y; :: thesis: { (f " {y}) where y is Element of Y : y in rng f } is a_partition of X
set P = { (f " {y}) where y is Element of Y : y in rng f } ;
for x being object holds
( x in X iff ex A being set st
( x in A & A in { (f " {y}) where y is Element of Y : y in rng f } ) )

proof

let x be object ; :: thesis: ( x in X iff ex A being set st
( x in A & A in { (f " {y}) where y is Element of Y : y in rng f } ) )

hereby :: thesis: ( ex A being set st
( x in A & A in { (f " {y}) where y is Element of Y : y in rng f } ) implies x in X )

assume A1: x in X ; :: thesis: ex A being set st
( x in A & A in { (f " {y}) where y is Element of Y : y in rng f } )
then A2: ( f . x in rng f & f . x in Y ) by FUNCT_2:4, FUNCT_2:5;
reconsider A = f " {(f . x)} as set ;
take A = A; :: thesis: ( x in A & A in { (f " {y}) where y is Element of Y : y in rng f } )
f . x in {(f . x)} by TARSKI:def 1;
hence x in A by A1, FUNCT_2:38; :: thesis: A in { (f " {y}) where y is Element of Y : y in rng f }
thus A in { (f " {y}) where y is Element of Y : y in rng f } by A2; :: thesis: verum

end;

given A being set such that A3: ( x in A & A in { (f " {y}) where y is Element of Y : y in rng f } ) ; :: thesis: x in X
consider y being Element of Y such that
A4: ( f " {y} = A & y in rng f ) by A3;
thus x in X by A3, A4; :: thesis: verum

end;

then A5: union { (f " {y}) where y is Element of Y : y in rng f } = X by TARSKI:def 4;
A6: for A being Subset of X st A in { (f " {y}) where y is Element of Y : y in rng f } holds
( A <> {} & ( for B being Subset of X holds
( not B in { (f " {y}) where y is Element of Y : y in rng f } or A = B or A misses B ) ) )

proof

let A be Subset of X; :: thesis: ( A in { (f " {y}) where y is Element of Y : y in rng f } implies ( A <> {} & ( for B being Subset of X holds
( not B in { (f " {y}) where y is Element of Y : y in rng f } or A = B or A misses B ) ) ) )
assume A in { (f " {y}) where y is Element of Y : y in rng f } ; :: thesis: ( A <> {} & ( for B being Subset of X holds
( not B in { (f " {y}) where y is Element of Y : y in rng f } or A = B or A misses B ) ) )
then consider y1 being Element of Y such that
A7: ( A = f " {y1} & y1 in rng f ) ;
consider x being object such that
A8: ( x in X & y1 = f . x ) by A7, FUNCT_2:11;
f . x in {y1} by A8, TARSKI:def 1;
hence A <> {} by A7, A8, FUNCT_2:38; :: thesis: for B being Subset of X holds
( not B in { (f " {y}) where y is Element of Y : y in rng f } or A = B or A misses B )
let B be Subset of X; :: thesis: ( not B in { (f " {y}) where y is Element of Y : y in rng f } or A = B or A misses B )
assume B in { (f " {y}) where y is Element of Y : y in rng f } ; :: thesis: ( A = B or A misses B )
then ex y2 being Element of Y st
( B = f " {y2} & y2 in rng f ) ;
hence ( A = B or A misses B ) by A7, ZFMISC_1:11, FUNCT_1:71; :: thesis: verum

end;

{ (f " {y}) where y is Element of Y : y in rng f } c= bool X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (f " {y}) where y is Element of Y : y in rng f } or x in bool X )
assume x in { (f " {y}) where y is Element of Y : y in rng f } ; :: thesis: x in bool X
then ex y being Element of Y st
( f " {y} = x & y in rng f ) ;
hence x in bool X ; :: thesis: verum

end;

hence { (f " {y}) where y is Element of Y : y in rng f } is a_partition of X by A5, A6, EQREL_1:def 4; :: thesis: verum