let f be non empty Function; :: thesis: for P being a_partition of dom f holds { (f | a) where a is Element of P : verum } is a_partition of f
set X = dom f;
let P be a_partition of dom f; :: thesis: { (f | a) where a is Element of P : verum } is a_partition of f
set Y = f;
set Q = { (f | a) where a is Element of P : verum } ;
{ (f | a) where a is Element of P : verum } c= bool f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (f | a) where a is Element of P : verum } or x in bool f )
reconsider xx = x as set by TARSKI:1;
assume x in { (f | a) where a is Element of P : verum } ; :: thesis: x in bool f
then ex p being Element of P st x = f | p ;
then xx c= f by RELAT_1:59;
hence x in bool f ; :: thesis: verum

end;

then reconsider Q = { (f | a) where a is Element of P : verum } as Subset-Family of f ;
Q is a_partition of f

proof

f c= union Q

proof

let y, z be object ; :: according to RELAT_1:def 3 :: thesis: ( not [y,z] in f or [y,z] in union Q )
assume A1: [y,z] in f ; :: thesis: [y,z] in union Q
then A2: y in dom f by XTUPLE_0:def 12;
dom f = union P by EQREL_1:def 4;
then consider p being set such that
A3: y in p and
A4: p in P by A2, TARSKI:def 4;
A5: [y,z] in f | p by A1, A3, RELAT_1:def 11;
f | p in Q by A4;
hence [y,z] in union Q by A5, TARSKI:def 4; :: thesis: verum

end;

hence f = union Q ; :: according to EQREL_1:def 4 :: thesis: for b₁ being Element of bool f holds
( not b₁ in Q or ( not b₁ = {} & ( for b₂ being Element of bool f holds
( not b₂ in Q or b₁ = b₂ or b₁ misses b₂ ) ) ) )
let A be Subset of f; :: thesis: ( not A in Q or ( not A = {} & ( for b₁ being Element of bool f holds
( not b₁ in Q or A = b₁ or A misses b₁ ) ) ) )
assume A in Q ; :: thesis: ( not A = {} & ( for b₁ being Element of bool f holds
( not b₁ in Q or A = b₁ or A misses b₁ ) ) )
then consider p being Element of P such that
A6: A = f | p ;
reconsider p = p as non empty Subset of (dom f) ;
thus A <> {} by A6; :: thesis: for b₁ being Element of bool f holds
( not b₁ in Q or A = b₁ or A misses b₁ )
let B be Subset of f; :: thesis: ( not B in Q or A = B or A misses B )
assume B in Q ; :: thesis: ( A = B or A misses B )
then consider p1 being Element of P such that
A7: B = f | p1 ;
assume A <> B ; :: thesis: A misses B
then A8: p misses p1 by A6, A7, EQREL_1:def 4;
assume A meets B ; :: thesis: contradiction
then consider x being object such that
A9: x in A and
A10: x in B by XBOOLE_0:3;
consider y, z being object such that
A11: x = [y,z] by A9, RELAT_1:def 1;
A12: y in p by A6, A9, A11, RELAT_1:def 11;
y in p1 by A7, A10, A11, RELAT_1:def 11;
hence contradiction by A8, A12, XBOOLE_0:3; :: thesis: verum

end;

hence { (f | a) where a is Element of P : verum } is a_partition of f ; :: thesis: verum