let Y be non empty set ; :: thesis: for G being Subset of (PARTITIONS Y)
for a, u being Function of Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
Ex ((u '&' a),PA,G) = u '&' (Ex (a,PA,G))
let G be Subset of (PARTITIONS Y); :: thesis: for a, u being Function of Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
Ex ((u '&' a),PA,G) = u '&' (Ex (a,PA,G))
let a, u be Function of Y,BOOLEAN; :: thesis: for PA being a_partition of Y st u is_independent_of PA,G holds
Ex ((u '&' a),PA,G) = u '&' (Ex (a,PA,G))
let PA be a_partition of Y; :: thesis: ( u is_independent_of PA,G implies Ex ((u '&' a),PA,G) = u '&' (Ex (a,PA,G)) )
assume A1: u is_independent_of PA,G ; :: thesis: Ex ((u '&' a),PA,G) = u '&' (Ex (a,PA,G))
A2: Ex ((u '&' a),PA,G) '<' u '&' (Ex (a,PA,G))

proof

let z be Element of Y; :: according to BVFUNC_1:def 12 :: thesis: ( not (Ex ((u '&' a),PA,G)) . z = TRUE or (u '&' (Ex (a,PA,G))) . z = TRUE )
assume (Ex ((u '&' a),PA,G)) . z = TRUE ; :: thesis: (u '&' (Ex (a,PA,G))) . z = TRUE
then consider x1 being Element of Y such that
A3: x1 in EqClass (z,(CompF (PA,G))) and
A4: (u '&' a) . x1 = TRUE by BVFUNC_1:def 17;
A5: (u . x1) '&' (a . x1) = TRUE by A4, MARGREL1:def 20;
then a . x1 = TRUE by MARGREL1:12;
then A6: (Ex (a,PA,G)) . z = TRUE by A3, BVFUNC_1:def 17;
z in EqClass (z,(CompF (PA,G))) by EQREL_1:def 6;
then A7: u . z = u . x1 by A1, A3, BVFUNC_1:def 15;
u . x1 = TRUE by A5, MARGREL1:12;
then (u '&' (Ex (a,PA,G))) . z = TRUE '&' TRUE by A6, A7, MARGREL1:def 20
.= TRUE ;
hence (u '&' (Ex (a,PA,G))) . z = TRUE ; :: thesis: verum

end;

u '&' (Ex (a,PA,G)) '<' Ex ((u '&' a),PA,G)

proof

let z be Element of Y; :: according to BVFUNC_1:def 12 :: thesis: ( not (u '&' (Ex (a,PA,G))) . z = TRUE or (Ex ((u '&' a),PA,G)) . z = TRUE )
assume (u '&' (Ex (a,PA,G))) . z = TRUE ; :: thesis: (Ex ((u '&' a),PA,G)) . z = TRUE
then A8: (u . z) '&' ((Ex (a,PA,G)) . z) = TRUE by MARGREL1:def 20;
then A9: u . z = TRUE by MARGREL1:12;
(Ex (a,PA,G)) . z = TRUE by A8, MARGREL1:12;
then consider x1 being Element of Y such that
A10: x1 in EqClass (z,(CompF (PA,G))) and
A11: a . x1 = TRUE by BVFUNC_1:def 17;
z in EqClass (z,(CompF (PA,G))) by EQREL_1:def 6;
then u . x1 = u . z by A1, A10, BVFUNC_1:def 15;
then (u '&' a) . x1 = TRUE '&' TRUE by A9, A11, MARGREL1:def 20
.= TRUE ;
hence (Ex ((u '&' a),PA,G)) . z = TRUE by A10, BVFUNC_1:def 17; :: thesis: verum

end;

hence Ex ((u '&' a),PA,G) = u '&' (Ex (a,PA,G)) by A2, BVFUNC_1:15; :: thesis: verum