let Y be non empty set ; :: thesis: for G being Subset of (PARTITIONS Y)
for a being Element of Funcs Y,BOOLEAN
for PA being a_partition of Y holds Ex a,PA,G is_dependent_of CompF PA,G
let G be Subset of (PARTITIONS Y); :: thesis: for a being Element of Funcs Y,BOOLEAN
for PA being a_partition of Y holds Ex a,PA,G is_dependent_of CompF PA,G
let a be Element of Funcs Y,BOOLEAN ; :: thesis: for PA being a_partition of Y holds Ex a,PA,G is_dependent_of CompF PA,G
let PA be a_partition of Y; :: thesis: Ex a,PA,G is_dependent_of CompF PA,G
let F be set ; :: according to BVFUNC_1:def 18 :: thesis: ( not F in CompF PA,G or for b₁, b₂ being set holds
( not b₁ in F or not b₂ in F or (Ex a,PA,G) . b₁ = (Ex a,PA,G) . b₂ ) )
assume A1: F in CompF PA,G ; :: thesis: for b₁, b₂ being set holds
( not b₁ in F or not b₂ in F or (Ex a,PA,G) . b₁ = (Ex a,PA,G) . b₂ )
thus for x1, x2 being set st x1 in F & x2 in F holds
(Ex a,PA,G) . x1 = (Ex a,PA,G) . x2 :: thesis: verum

proof

let x1, x2 be set ; :: thesis: ( x1 in F & x2 in F implies (Ex a,PA,G) . x1 = (Ex a,PA,G) . x2 )
assume A2: ( x1 in F & x2 in F ) ; :: thesis: (Ex a,PA,G) . x1 = (Ex 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 8;
( F = EqClass x2,(CompF PA,G) or F misses EqClass x2,(CompF PA,G) ) by A1, EQREL_1:def 6;
then A4: EqClass x1,(CompF PA,G) = EqClass x2,(CompF PA,G) by A2, A3, EQREL_1:def 8, XBOOLE_0:3;

per cases ( ( ex x being Element of Y st
( x in EqClass x1,(CompF PA,G) & a . x = TRUE ) & ex x being Element of Y st
( x in EqClass x2,(CompF PA,G) & a . x = TRUE ) ) or ( ex x being Element of Y st
( x in EqClass x1,(CompF PA,G) & a . x = TRUE ) & ( for x being Element of Y holds
( not x in EqClass x2,(CompF PA,G) or not a . x = TRUE ) ) ) or ( ( for x being Element of Y holds
( not x in EqClass x1,(CompF PA,G) or not a . x = TRUE ) ) & ex x being Element of Y st
( x in EqClass x2,(CompF PA,G) & a . x = TRUE ) ) or ( ( for x being Element of Y holds
( not x in EqClass x1,(CompF PA,G) or not a . x = TRUE ) ) & ( for x being Element of Y holds
( not x in EqClass x2,(CompF PA,G) or not a . x = TRUE ) ) ) ) ;

suppose A5: ( ex x being Element of Y st
( x in EqClass x1,(CompF PA,G) & a . x = TRUE ) & ex x being Element of Y st
( x in EqClass x2,(CompF PA,G) & a . x = TRUE ) ) ; :: thesis: (Ex a,PA,G) . x1 = (Ex a,PA,G) . x2

then (B_SUP a,(CompF PA,G)) . x1 = TRUE by BVFUNC_1:def 20;
hence (Ex a,PA,G) . x1 = (Ex a,PA,G) . x2 by A5, BVFUNC_1:def 20; :: thesis: verum

end;

suppose ( ex x being Element of Y st
( x in EqClass x1,(CompF PA,G) & a . x = TRUE ) & ( for x being Element of Y holds
( not x in EqClass x2,(CompF PA,G) or not a . x = TRUE ) ) ) ; :: thesis: (Ex a,PA,G) . x1 = (Ex a,PA,G) . x2

hence (Ex a,PA,G) . x1 = (Ex a,PA,G) . x2 by A4; :: thesis: verum

end;

suppose ( ( for x being Element of Y holds
( not x in EqClass x1,(CompF PA,G) or not a . x = TRUE ) ) & ex x being Element of Y st
( x in EqClass x2,(CompF PA,G) & a . x = TRUE ) ) ; :: thesis: (Ex a,PA,G) . x1 = (Ex a,PA,G) . x2

hence (Ex a,PA,G) . x1 = (Ex a,PA,G) . x2 by A4; :: thesis: verum

end;

suppose A6: ( ( for x being Element of Y holds
( not x in EqClass x1,(CompF PA,G) or not a . x = TRUE ) ) & ( for x being Element of Y holds
( not x in EqClass x2,(CompF PA,G) or not a . x = TRUE ) ) ) ; :: thesis: (Ex a,PA,G) . x1 = (Ex a,PA,G) . x2

then (B_SUP a,(CompF PA,G)) . x1 = FALSE by BVFUNC_1:def 20;
hence (Ex a,PA,G) . x1 = (Ex a,PA,G) . x2 by A6, BVFUNC_1:def 20; :: thesis: verum

end;

end;

end;