let Y be non empty set ; :: thesis: for G being Subset of ()
for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds All (a,PA,G) is_dependent_of CompF (PA,G)

let G be Subset of (); :: thesis: for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds All (a,PA,G) is_dependent_of CompF (PA,G)

let a be Function of Y,BOOLEAN; :: thesis: for PA being a_partition of Y holds All (a,PA,G) is_dependent_of CompF (PA,G)
let PA be a_partition of Y; :: thesis: All (a,PA,G) is_dependent_of CompF (PA,G)
let F be set ; :: according to BVFUNC_1:def 15 :: thesis: ( not F in CompF (PA,G) or for b1, b2 being set holds
( not b1 in F or not b2 in F or (All (a,PA,G)) . b1 = (All (a,PA,G)) . b2 ) )

assume A1: F in CompF (PA,G) ; :: thesis: for b1, b2 being set holds
( not b1 in F or not b2 in F or (All (a,PA,G)) . b1 = (All (a,PA,G)) . b2 )

thus for x1, x2 being set st x1 in F & x2 in F holds
(All (a,PA,G)) . x1 = (All (a,PA,G)) . x2 :: thesis: verum
proof
let x1, x2 be set ; :: thesis: ( x1 in F & x2 in F implies (All (a,PA,G)) . x1 = (All (a,PA,G)) . x2 )
assume A2: ( x1 in F & x2 in F ) ; :: thesis: (All (a,PA,G)) . x1 = (All (a,PA,G)) . x2
then reconsider x1 = x1, x2 = x2 as Element of Y by A1;
A3: x2 in EqClass (x2,(CompF (PA,G))) by EQREL_1:def 6;
( F = EqClass (x2,(CompF (PA,G))) or F misses EqClass (x2,(CompF (PA,G))) ) by ;
then A4: EqClass (x1,(CompF (PA,G))) = EqClass (x2,(CompF (PA,G))) by ;
per cases ( ( ( for x being Element of Y st x in EqClass (x1,(CompF (PA,G))) holds
a . x = TRUE ) & ( for x being Element of Y st x in EqClass (x2,(CompF (PA,G))) holds
a . x = TRUE ) ) or ( ( for x being Element of Y st x in EqClass (x1,(CompF (PA,G))) holds
a . x = TRUE ) & ex x being Element of Y st
( x in EqClass (x2,(CompF (PA,G))) & not a . x = TRUE ) ) or ( ex x being Element of Y st
( x in EqClass (x1,(CompF (PA,G))) & not a . x = TRUE ) & ( for x being Element of Y st x in EqClass (x2,(CompF (PA,G))) holds
a . x = TRUE ) ) or ( ex x being Element of Y st
( x in EqClass (x1,(CompF (PA,G))) & not a . x = TRUE ) & ex x being Element of Y st
( x in EqClass (x2,(CompF (PA,G))) & not a . x = TRUE ) ) )
;
suppose A5: ( ( for x being Element of Y st x in EqClass (x1,(CompF (PA,G))) holds
a . x = TRUE ) & ( for x being Element of Y st x in EqClass (x2,(CompF (PA,G))) holds
a . x = TRUE ) ) ; :: thesis: (All (a,PA,G)) . x1 = (All (a,PA,G)) . x2
then (All (a,PA,G)) . x2 = TRUE by BVFUNC_1:def 16;
hence (All (a,PA,G)) . x1 = (All (a,PA,G)) . x2 by ; :: thesis: verum
end;
suppose ( ( for x being Element of Y st x in EqClass (x1,(CompF (PA,G))) holds
a . x = TRUE ) & ex x being Element of Y st
( x in EqClass (x2,(CompF (PA,G))) & not a . x = TRUE ) ) ; :: thesis: (All (a,PA,G)) . x1 = (All (a,PA,G)) . x2
hence (All (a,PA,G)) . x1 = (All (a,PA,G)) . x2 by A4; :: thesis: verum
end;
suppose ( ex x being Element of Y st
( x in EqClass (x1,(CompF (PA,G))) & not a . x = TRUE ) & ( for x being Element of Y st x in EqClass (x2,(CompF (PA,G))) holds
a . x = TRUE ) ) ; :: thesis: (All (a,PA,G)) . x1 = (All (a,PA,G)) . x2
hence (All (a,PA,G)) . x1 = (All (a,PA,G)) . x2 by A4; :: thesis: verum
end;
suppose A6: ( ex x being Element of Y st
( x in EqClass (x1,(CompF (PA,G))) & not a . x = TRUE ) & ex x being Element of Y st
( x in EqClass (x2,(CompF (PA,G))) & not a . x = TRUE ) ) ; :: thesis: (All (a,PA,G)) . x1 = (All (a,PA,G)) . x2
then (All (a,PA,G)) . x2 = FALSE by BVFUNC_1:def 16;
hence (All (a,PA,G)) . x1 = (All (a,PA,G)) . x2 by ; :: thesis: verum
end;
end;
end;