let Y be non empty set ; :: thesis:
let G be Subset of (PARTITIONS Y); :: thesis:
let u, a be Element of Funcs (Y,BOOLEAN); :: thesis:
let PA be a_partition of Y; :: thesis:
consider k3 being Function such that
A1: All ((u 'or' a),PA,G) = k3 and
A2: dom k3 = Y and
rng k3 c= BOOLEAN by FUNCT_2:def 2;
consider k4 being Function such that
A3: u 'or' (All (a,PA,G)) = k4 and
A4: dom k4 = Y and
rng k4 c= BOOLEAN by FUNCT_2:def 2;
assume u is_independent_of PA,G ; :: thesis:
then A5: u is_dependent_of CompF (PA,G) by Def8;
for z being Element of Y holds (B_INF ((u 'or' a),(CompF (PA,G)))) . z = (u 'or' (B_INF (a,(CompF (PA,G))))) . z

let z be Element of Y; :: thesis:
A6: (u 'or' (B_INF (a,(CompF (PA,G))))) . z = (u . z) 'or' ((B_INF (a,(CompF (PA,G)))) . z) by BVFUNC_1:def 4;

let x be Element of Y; :: thesis:
assume A9: x in EqClass (z,(CompF (PA,G))) ; :: thesis:
(u 'or' a) . x = (u . x) 'or' (a . x) by BVFUNC_1:def 4
.= (u . x) 'or' TRUE by A7, A9
.= TRUE by BINARITH:10 ;
hence (u 'or' a) . x = TRUE ; :: thesis:

end;

end;

suppose A10: ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) & ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
u . x = TRUE ) ) ; :: thesis:

let x be Element of Y; :: thesis:
assume A12: x in EqClass (z,(CompF (PA,G))) ; :: thesis:
(u 'or' a) . x = (u . x) 'or' (a . x) by BVFUNC_1:def 4
.= TRUE 'or' (a . x) by A10, A12
.= TRUE by BINARITH:10 ;
hence (u 'or' a) . x = TRUE ; :: thesis:

end;

end;

suppose A13: ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not a . x = TRUE ) & ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not u . x = TRUE ) ) ; :: thesis:

end;

then for u being set st u in Y holds
k3 . u = k4 . u by A1, A3;
hence All ((u 'or' a),PA,G) = u 'or' (All (a,PA,G)) by A1, A2, A3, A4, FUNCT_1:2; :: thesis: