let Y be non empty set ; :: thesis: for G being Subset of (PARTITIONS Y)

for a being Function of 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 Function of Y,BOOLEAN

for PA being a_partition of Y holds Ex (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 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 15 :: thesis: ( not F in CompF (PA,G) or for b_{1}, b_{2} being set holds

( not b_{1} in F or not b_{2} in F or (Ex (a,PA,G)) . b_{1} = (Ex (a,PA,G)) . b_{2} ) )

assume A1: F in CompF (PA,G) ; :: thesis: for b_{1}, b_{2} being set holds

( not b_{1} in F or not b_{2} in F or (Ex (a,PA,G)) . b_{1} = (Ex (a,PA,G)) . b_{2} )

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

for a being Function of 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 Function of Y,BOOLEAN

for PA being a_partition of Y holds Ex (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 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 15 :: thesis: ( not F in CompF (PA,G) or for b

( not b

assume A1: F in CompF (PA,G) ; :: thesis: for b

( not 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 6;

( F = EqClass (x2,(CompF (PA,G))) or F misses EqClass (x2,(CompF (PA,G))) ) by A1, EQREL_1:def 4;

then A4: EqClass (x1,(CompF (PA,G))) = EqClass (x2,(CompF (PA,G))) by A2, A3, EQREL_1:def 6, XBOOLE_0:3;

end;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 6;

( F = EqClass (x2,(CompF (PA,G))) or F misses EqClass (x2,(CompF (PA,G))) ) by A1, EQREL_1:def 4;

then A4: EqClass (x1,(CompF (PA,G))) = EqClass (x2,(CompF (PA,G))) by A2, A3, EQREL_1:def 6, 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 ) ) ) ) ;

end;

( 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

( 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 17;

hence (Ex (a,PA,G)) . x1 = (Ex (a,PA,G)) . x2 by A5, BVFUNC_1:def 17; :: thesis: verum

end;hence (Ex (a,PA,G)) . x1 = (Ex (a,PA,G)) . x2 by A5, BVFUNC_1:def 17; :: thesis: verum

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

end;

( 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

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

end;

( 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

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

( 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 17;

hence (Ex (a,PA,G)) . x1 = (Ex (a,PA,G)) . x2 by A6, BVFUNC_1:def 17; :: thesis: verum

end;hence (Ex (a,PA,G)) . x1 = (Ex (a,PA,G)) . x2 by A6, BVFUNC_1:def 17; :: thesis: verum