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))

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

u '&' (Ex (a,PA,G)) '<' Ex ((u '&' a),PA,G)
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;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

proof

hence
Ex ((u '&' a),PA,G) = u '&' (Ex (a,PA,G))
by A2, BVFUNC_1:15; :: thesis: verum
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;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