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 ;
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 ; :: 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 ;
f . x in {y1} by ;
hence A <> {} by ; :: 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 ; :: 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 ; :: thesis: verum