let Y be non empty set ; :: thesis: for G being Subset of (PARTITIONS Y)
for u, a being Element of Funcs 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 u, a being Element of Funcs 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 u, a be Element of Funcs 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 15 :: 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 19;
(u '&' a) . x = (u . x) '&' (a . x) by MARGREL1:def 21;
hence u . x = TRUE by A4, MARGREL1:45; :: 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 19;
(u '&' a) . x = (u . x) '&' (a . x) by MARGREL1:def 21;
hence a . x = TRUE by A5, MARGREL1:45; :: 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 19, MARGREL1:def 21;
z in EqClass z,(CompF PA,G) by EQREL_1:def 8;
then u . z = TRUE by A3;
hence (u '&' (All a,PA,G)) . z = TRUE by A6; :: thesis: verum

end;

assume u is_independent_of PA,G ; :: thesis: All (u '&' a),PA,G = u '&' (All a,PA,G)
then A7: u is_dependent_of CompF PA,G by Def8;
u '&' (All a,PA,G) '<' All (u '&' a),PA,G

proof

let z be Element of Y; :: according to BVFUNC_1:def 15 :: 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 8;
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 21;
then A10: (All a,PA,G) . z = TRUE by MARGREL1:45;
A11: u . z = TRUE by A9, MARGREL1:45;
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 18, BVFUNC_1:def 19;
then (u '&' a) . x = TRUE '&' TRUE by A11, MARGREL1:def 21
.= TRUE ;
hence (u '&' a) . x = TRUE ; :: thesis: verum

end;

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

end;

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