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:
assume u is_independent_of PA,G ; :: thesis:
then A1: u is_dependent_of CompF PA,G by Def8;
let z be Element of Y; :: according to BVFUNC_1:def 15 :: thesis:
assume A2: (All (u 'xor' a),PA,G) . z = TRUE ; :: thesis:
A3: z in EqClass z,(CompF PA,G) by EQREL_1:def 8;
A4: ( 'not' FALSE = TRUE & (u 'xor' (All a,PA,G)) . z = ((All a,PA,G) . z) 'xor' (u . z) ) by BVFUNC_1:def 8, MARGREL1:41;

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

then A5: ( u . z = TRUE & a . z = TRUE ) by A3;
A6: FALSE '&' TRUE = FALSE by MARGREL1:45;
(u 'xor' a) . z = (a . z) 'xor' (u . z) by BVFUNC_1:def 8
.= FALSE by A5, A6, MARGREL1:41 ;
hence (u 'xor' (All a,PA,G)) . z = TRUE by A2, A3, BVFUNC_1:def 19; :: thesis:

end;

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

then consider x1 being Element of Y such that
A8: x1 in EqClass z,(CompF PA,G) and
a . x1 <> TRUE ;
A9: u . x1 = TRUE by A7, A8;
A10: (All a,PA,G) . z = FALSE by A7, BVFUNC_1:def 19;
u . z = u . x1 by A1, A3, A8, BVFUNC_1:def 18;
then (u 'xor' (All a,PA,G)) . z = TRUE 'or' FALSE by A4, A10, A9
.= TRUE by BINARITH:7 ;
hence (u 'xor' (All a,PA,G)) . z = TRUE ; :: thesis:

end;

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

then consider x1 being Element of Y such that
A11: x1 in EqClass z,(CompF PA,G) and
A12: u . x1 <> TRUE ;

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

u . z = u . x1 by A1, A3, A11, BVFUNC_1:def 18;
then A14: u . z = FALSE by A12, XBOOLEAN:def 3;
(All a,PA,G) . z = TRUE by A13, BVFUNC_1:def 19;
then (u 'xor' (All a,PA,G)) . z = FALSE 'or' TRUE by A4, A14
.= TRUE by BINARITH:7 ;
hence (u 'xor' (All a,PA,G)) . z = TRUE ; :: thesis:

end;

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

then consider x2 being Element of Y such that
A15: x2 in EqClass z,(CompF PA,G) and
A16: a . x2 <> TRUE ;
A17: a . x2 = FALSE by A16, XBOOLEAN:def 3;
u . x1 = u . x2 by A1, A11, A15, BVFUNC_1:def 18;
then A18: u . x2 = FALSE by A12, XBOOLEAN:def 3;
(u 'xor' a) . x2 = (a . x2) 'xor' (u . x2) by BVFUNC_1:def 8
.= FALSE by A18, A17, MARGREL1:45 ;
hence (u 'xor' (All a,PA,G)) . z = TRUE by A2, A15, BVFUNC_1:def 19; :: thesis:

end;

end;

end;

hence (u 'xor' (All a,PA,G)) . z = TRUE ; :: thesis:

end;

end;