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
All ((u '&' a),PA,G) = u '&' (All (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
All ((u '&' a),PA,G) = u '&' (All (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
All ((u '&' a),PA,G) = u '&' (All (a,PA,G))
let PA be a_partition of Y; :: thesis: ( u is_independent_of PA,G implies All ((u '&' a),PA,G) = u '&' (All (a,PA,G)) )
A1: All ((u '&' a),PA,G) '<' u '&' (All (a,PA,G))

proof

let z be Element of Y; :: according to BVFUNC_1:def 12 :: thesis: ( not (All ((u '&' a),PA,G)) . z = TRUE or (u '&' (All (a,PA,G))) . z = TRUE )
assume A2: (All ((u '&' a),PA,G)) . z = TRUE ; :: thesis: (u '&' (All (a,PA,G))) . z = TRUE
A3: for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
u . x = TRUE

proof

let x be Element of Y; :: thesis: ( x in EqClass (z,(CompF (PA,G))) implies u . x = TRUE )
assume x in EqClass (z,(CompF (PA,G))) ; :: thesis: u . x = TRUE
then A4: (u '&' a) . x = TRUE by A2, BVFUNC_1:def 16;
(u '&' a) . x = (u . x) '&' (a . x) by MARGREL1:def 20;
hence u . x = TRUE by A4, MARGREL1:12; :: thesis: verum

end;

for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
a . x = TRUE

proof

let x be Element of Y; :: thesis: ( x in EqClass (z,(CompF (PA,G))) implies a . x = TRUE )
assume x in EqClass (z,(CompF (PA,G))) ; :: thesis: a . x = TRUE
then A5: (u '&' a) . x = TRUE by A2, BVFUNC_1:def 16;
(u '&' a) . x = (u . x) '&' (a . x) by MARGREL1:def 20;
hence a . x = TRUE by A5, MARGREL1:12; :: thesis: verum

end;

then A6: ( (u '&' (All (a,PA,G))) . z = (u . z) '&' ((All (a,PA,G)) . z) & (All (a,PA,G)) . z = TRUE ) by BVFUNC_1:def 16, MARGREL1:def 20;
u . z = TRUE by A3, EQREL_1:def 6;
hence (u '&' (All (a,PA,G))) . z = TRUE by A6; :: thesis: verum

end;

assume A7: u is_independent_of PA,G ; :: thesis: All ((u '&' a),PA,G) = u '&' (All (a,PA,G))
u '&' (All (a,PA,G)) '<' All ((u '&' a),PA,G)

proof

let z be Element of Y; :: according to BVFUNC_1:def 12 :: thesis: ( not (u '&' (All (a,PA,G))) . z = TRUE or (All ((u '&' a),PA,G)) . z = TRUE )
A8: z in EqClass (z,(CompF (PA,G))) by EQREL_1:def 6;
assume (u '&' (All (a,PA,G))) . z = TRUE ; :: thesis: (All ((u '&' a),PA,G)) . z = TRUE
then A9: (u . z) '&' ((All (a,PA,G)) . z) = TRUE by MARGREL1:def 20;
then A10: (All (a,PA,G)) . z = TRUE by MARGREL1:12;
A11: u . z = TRUE by A9, MARGREL1:12;
for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
(u '&' a) . x = TRUE

proof

let x be Element of Y; :: thesis: ( x in EqClass (z,(CompF (PA,G))) implies (u '&' a) . x = TRUE )
assume x in EqClass (z,(CompF (PA,G))) ; :: thesis: (u '&' a) . x = TRUE
then ( a . x = TRUE & u . x = u . z ) by A7, A10, A8, BVFUNC_1:def 15, BVFUNC_1:def 16;
then (u '&' a) . x = TRUE '&' TRUE by A11, MARGREL1:def 20
.= TRUE ;
hence (u '&' a) . x = TRUE ; :: thesis: verum

end;

hence (All ((u '&' a),PA,G)) . z = TRUE by BVFUNC_1:def 16; :: thesis: verum

end;

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