let Y be non empty set ; for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for P, Q being a_partition of Y st G is independent holds
All (All a,P,G),Q,G = All (All a,Q,G),P,G
let a be Element of Funcs Y,BOOLEAN ; for G being Subset of (PARTITIONS Y)
for P, Q being a_partition of Y st G is independent holds
All (All a,P,G),Q,G = All (All a,Q,G),P,G
let G be Subset of (PARTITIONS Y); for P, Q being a_partition of Y st G is independent holds
All (All a,P,G),Q,G = All (All a,Q,G),P,G
let P, Q be a_partition of Y; ( G is independent implies All (All a,P,G),Q,G = All (All a,Q,G),P,G )
set A = G \ {P};
set B = G \ {Q};
A1:
CompF P,G = '/\' (G \ {P})
by BVFUNC_2:def 7;
A2:
( G \ {P} c= G & G \ {Q} c= G )
by XBOOLE_1:36;
A3:
CompF Q,G = '/\' (G \ {Q})
by BVFUNC_2:def 7;
assume
G is independent
; All (All a,P,G),Q,G = All (All a,Q,G),P,G
then A4:
(ERl ('/\' (G \ {P}))) * (ERl ('/\' (G \ {Q}))) = (ERl ('/\' (G \ {Q}))) * (ERl ('/\' (G \ {P})))
by A2, Th16;
A5:
for y being Element of Y holds
( ( ( for x being Element of Y st x in EqClass y,(CompF Q,G) holds
(B_INF a,(CompF P,G)) . x = TRUE ) implies (B_INF (B_INF a,(CompF Q,G)),(CompF P,G)) . y = TRUE ) & ( ex x being Element of Y st
( x in EqClass y,(CompF Q,G) & not (B_INF a,(CompF P,G)) . x = TRUE ) implies (B_INF (B_INF a,(CompF Q,G)),(CompF P,G)) . y = FALSE ) )
proof
let y be
Element of
Y;
( ( ( for x being Element of Y st x in EqClass y,(CompF Q,G) holds
(B_INF a,(CompF P,G)) . x = TRUE ) implies (B_INF (B_INF a,(CompF Q,G)),(CompF P,G)) . y = TRUE ) & ( ex x being Element of Y st
( x in EqClass y,(CompF Q,G) & not (B_INF a,(CompF P,G)) . x = TRUE ) implies (B_INF (B_INF a,(CompF Q,G)),(CompF P,G)) . y = FALSE ) )
hereby ( ex x being Element of Y st
( x in EqClass y,(CompF Q,G) & not (B_INF a,(CompF P,G)) . x = TRUE ) implies (B_INF (B_INF a,(CompF Q,G)),(CompF P,G)) . y = FALSE )
assume A6:
for
x being
Element of
Y st
x in EqClass y,
(CompF Q,G) holds
(B_INF a,(CompF P,G)) . x = TRUE
;
(B_INF (B_INF a,(CompF Q,G)),(CompF P,G)) . y = TRUE
for
x being
Element of
Y st
x in EqClass y,
(CompF P,G) holds
(B_INF a,(CompF Q,G)) . x = TRUE
proof
let x be
Element of
Y;
( x in EqClass y,(CompF P,G) implies (B_INF a,(CompF Q,G)) . x = TRUE )
assume
x in EqClass y,
(CompF P,G)
;
(B_INF a,(CompF Q,G)) . x = TRUE
then A7:
[x,y] in ERl ('/\' (G \ {P}))
by A1, Th5;
for
z being
Element of
Y st
z in EqClass x,
(CompF Q,G) holds
a . z = TRUE
proof
let z be
Element of
Y;
( z in EqClass x,(CompF Q,G) implies a . z = TRUE )
assume
z in EqClass x,
(CompF Q,G)
;
a . z = TRUE
then
[z,x] in ERl ('/\' (G \ {Q}))
by A3, Th5;
then
[z,y] in (ERl ('/\' (G \ {P}))) * (ERl ('/\' (G \ {Q})))
by A4, A7, RELAT_1:def 8;
then consider u being
set such that A8:
[z,u] in ERl ('/\' (G \ {P}))
and A9:
[u,y] in ERl ('/\' (G \ {Q}))
by RELAT_1:def 8;
u in field (ERl ('/\' (G \ {Q})))
by A9, RELAT_1:30;
then reconsider u =
u as
Element of
Y by ORDERS_1:97;
u in EqClass y,
(CompF Q,G)
by A3, A9, Th5;
then A10:
(B_INF a,(CompF P,G)) . u <> FALSE
by A6;
z in EqClass u,
(CompF P,G)
by A1, A8, Th5;
hence
a . z = TRUE
by A10, BVFUNC_1:def 19;
verum
end;
hence
(B_INF a,(CompF Q,G)) . x = TRUE
by BVFUNC_1:def 19;
verum
end; hence
(B_INF (B_INF a,(CompF Q,G)),(CompF P,G)) . y = TRUE
by BVFUNC_1:def 19;
verum
end;
given x being
Element of
Y such that A11:
x in EqClass y,
(CompF Q,G)
and A12:
(B_INF a,(CompF P,G)) . x <> TRUE
;
(B_INF (B_INF a,(CompF Q,G)),(CompF P,G)) . y = FALSE
consider z being
Element of
Y such that A13:
z in EqClass x,
(CompF P,G)
and A14:
a . z <> TRUE
by A12, BVFUNC_1:def 19;
A15:
[x,y] in ERl ('/\' (G \ {Q}))
by A3, A11, Th5;
[z,x] in ERl ('/\' (G \ {P}))
by A1, A13, Th5;
then
[z,y] in (ERl ('/\' (G \ {Q}))) * (ERl ('/\' (G \ {P})))
by A4, A15, RELAT_1:def 8;
then consider u being
set such that A16:
[z,u] in ERl ('/\' (G \ {Q}))
and A17:
[u,y] in ERl ('/\' (G \ {P}))
by RELAT_1:def 8;
u in field (ERl ('/\' (G \ {Q})))
by A16, RELAT_1:30;
then reconsider u =
u as
Element of
Y by ORDERS_1:97;
z in EqClass u,
(CompF Q,G)
by A3, A16, Th5;
then A18:
(B_INF a,(CompF Q,G)) . u = FALSE
by A14, BVFUNC_1:def 19;
u in EqClass y,
(CompF P,G)
by A1, A17, Th5;
hence
(B_INF (B_INF a,(CompF Q,G)),(CompF P,G)) . y = FALSE
by A18, BVFUNC_1:def 19;
verum
end;
thus All (All a,P,G),Q,G =
B_INF (All a,P,G),(CompF Q,G)
by BVFUNC_2:def 9
.=
B_INF (B_INF a,(CompF P,G)),(CompF Q,G)
by BVFUNC_2:def 9
.=
B_INF (B_INF a,(CompF Q,G)),(CompF P,G)
by A5, BVFUNC_1:def 19
.=
B_INF (All a,Q,G),(CompF P,G)
by BVFUNC_2:def 9
.=
All (All a,Q,G),P,G
by BVFUNC_2:def 9
; verum