let Y be non empty set ; :: thesis: for PA, PB being a_partition of Y

for p0, x, y being set

for f being FinSequence of Y st p0 c= Y & x in p0 & f . 1 = x & f . (len f) = y & 1 <= len f & ( for i being Nat st 1 <= i & i < len f holds

ex p2, p3, u being set st

( p2 in PA & p3 in PB & f . i in p2 & u in p2 & u in p3 & f . (i + 1) in p3 ) ) & p0 is_a_dependent_set_of PA & p0 is_a_dependent_set_of PB holds

y in p0

let PA, PB be a_partition of Y; :: thesis: for p0, x, y being set

for f being FinSequence of Y st p0 c= Y & x in p0 & f . 1 = x & f . (len f) = y & 1 <= len f & ( for i being Nat st 1 <= i & i < len f holds

ex p2, p3, u being set st

( p2 in PA & p3 in PB & f . i in p2 & u in p2 & u in p3 & f . (i + 1) in p3 ) ) & p0 is_a_dependent_set_of PA & p0 is_a_dependent_set_of PB holds

y in p0

let p0, x, y be set ; :: thesis: for f being FinSequence of Y st p0 c= Y & x in p0 & f . 1 = x & f . (len f) = y & 1 <= len f & ( for i being Nat st 1 <= i & i < len f holds

ex p2, p3, u being set st

( p2 in PA & p3 in PB & f . i in p2 & u in p2 & u in p3 & f . (i + 1) in p3 ) ) & p0 is_a_dependent_set_of PA & p0 is_a_dependent_set_of PB holds

y in p0

let f be FinSequence of Y; :: thesis: ( p0 c= Y & x in p0 & f . 1 = x & f . (len f) = y & 1 <= len f & ( for i being Nat st 1 <= i & i < len f holds

ex p2, p3, u being set st

( p2 in PA & p3 in PB & f . i in p2 & u in p2 & u in p3 & f . (i + 1) in p3 ) ) & p0 is_a_dependent_set_of PA & p0 is_a_dependent_set_of PB implies y in p0 )

assume that

A1: p0 c= Y and

A2: ( x in p0 & f . 1 = x ) and

A3: ( f . (len f) = y & 1 <= len f ) and

A4: for i being Nat st 1 <= i & i < len f holds

ex p2, p3, u being set st

( p2 in PA & p3 in PB & f . i in p2 & u in p2 & u in p3 & f . (i + 1) in p3 ) and

A5: p0 is_a_dependent_set_of PA and

A6: p0 is_a_dependent_set_of PB ; :: thesis: y in p0

consider A1 being set such that

A7: A1 c= PA and

A1 <> {} and

A8: p0 = union A1 by A5;

consider B1 being set such that

A9: B1 c= PB and

B1 <> {} and

A10: p0 = union B1 by A6;

A11: union PA = Y by EQREL_1:def 4;

A12: for A being set st A in PA holds

( A <> {} & ( for B being set holds

( not B in PA or A = B or A misses B ) ) ) by EQREL_1:def 4;

A13: for A being set st A in PB holds

( A <> {} & ( for B being set holds

( not B in PB or A = B or A misses B ) ) ) by EQREL_1:def 4;

for k being Nat st 1 <= k & k <= len f holds

f . k in p0

for p0, x, y being set

for f being FinSequence of Y st p0 c= Y & x in p0 & f . 1 = x & f . (len f) = y & 1 <= len f & ( for i being Nat st 1 <= i & i < len f holds

ex p2, p3, u being set st

( p2 in PA & p3 in PB & f . i in p2 & u in p2 & u in p3 & f . (i + 1) in p3 ) ) & p0 is_a_dependent_set_of PA & p0 is_a_dependent_set_of PB holds

y in p0

let PA, PB be a_partition of Y; :: thesis: for p0, x, y being set

for f being FinSequence of Y st p0 c= Y & x in p0 & f . 1 = x & f . (len f) = y & 1 <= len f & ( for i being Nat st 1 <= i & i < len f holds

ex p2, p3, u being set st

( p2 in PA & p3 in PB & f . i in p2 & u in p2 & u in p3 & f . (i + 1) in p3 ) ) & p0 is_a_dependent_set_of PA & p0 is_a_dependent_set_of PB holds

y in p0

let p0, x, y be set ; :: thesis: for f being FinSequence of Y st p0 c= Y & x in p0 & f . 1 = x & f . (len f) = y & 1 <= len f & ( for i being Nat st 1 <= i & i < len f holds

ex p2, p3, u being set st

( p2 in PA & p3 in PB & f . i in p2 & u in p2 & u in p3 & f . (i + 1) in p3 ) ) & p0 is_a_dependent_set_of PA & p0 is_a_dependent_set_of PB holds

y in p0

let f be FinSequence of Y; :: thesis: ( p0 c= Y & x in p0 & f . 1 = x & f . (len f) = y & 1 <= len f & ( for i being Nat st 1 <= i & i < len f holds

ex p2, p3, u being set st

( p2 in PA & p3 in PB & f . i in p2 & u in p2 & u in p3 & f . (i + 1) in p3 ) ) & p0 is_a_dependent_set_of PA & p0 is_a_dependent_set_of PB implies y in p0 )

assume that

A1: p0 c= Y and

A2: ( x in p0 & f . 1 = x ) and

A3: ( f . (len f) = y & 1 <= len f ) and

A4: for i being Nat st 1 <= i & i < len f holds

ex p2, p3, u being set st

( p2 in PA & p3 in PB & f . i in p2 & u in p2 & u in p3 & f . (i + 1) in p3 ) and

A5: p0 is_a_dependent_set_of PA and

A6: p0 is_a_dependent_set_of PB ; :: thesis: y in p0

consider A1 being set such that

A7: A1 c= PA and

A1 <> {} and

A8: p0 = union A1 by A5;

consider B1 being set such that

A9: B1 c= PB and

B1 <> {} and

A10: p0 = union B1 by A6;

A11: union PA = Y by EQREL_1:def 4;

A12: for A being set st A in PA holds

( A <> {} & ( for B being set holds

( not B in PA or A = B or A misses B ) ) ) by EQREL_1:def 4;

A13: for A being set st A in PB holds

( A <> {} & ( for B being set holds

( not B in PB or A = B or A misses B ) ) ) by EQREL_1:def 4;

for k being Nat st 1 <= k & k <= len f holds

f . k in p0

proof

hence
y in p0
by A3; :: thesis: verum
defpred S_{1}[ Nat] means ( 1 <= $1 & $1 <= len f implies f . $1 in p0 );

A14: S_{1}[ 0 ]
;

A15: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[k]
from NAT_1:sch 2(A14, A15); :: thesis: verum

end;A14: S

A15: for k being Nat st S

S

proof

thus
for k being Nat holds S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A16: S_{1}[k]
; :: thesis: S_{1}[k + 1]

assume that

A17: 1 <= k + 1 and

A18: k + 1 <= len f ; :: thesis: f . (k + 1) in p0

A19: k < len f by A18, NAT_1:13;

A20: ( 1 <= k or 1 = k + 1 ) by A17, NAT_1:8;

end;assume A16: S

assume that

A17: 1 <= k + 1 and

A18: k + 1 <= len f ; :: thesis: f . (k + 1) in p0

A19: k < len f by A18, NAT_1:13;

A20: ( 1 <= k or 1 = k + 1 ) by A17, NAT_1:8;

now :: thesis: f . (k + 1) in p0end;

hence
f . (k + 1) in p0
; :: thesis: verumper cases
( 1 <= k or 0 = k )
by A20;

end;

suppose A21:
1 <= k
; :: thesis: f . (k + 1) in p0

then consider p2, p3, u being set such that

A22: p2 in PA and

A23: p3 in PB and

A24: f . k in p2 and

A25: u in p2 and

A26: u in p3 and

A27: f . (k + 1) in p3 by A4, A19;

consider A being set such that

A28: f . k in A and

A29: A in PA by A1, A11, A16, A18, A21, NAT_1:13, TARSKI:def 4;

A30: ( p2 = A or p2 misses A ) by A22, A29, EQREL_1:def 4;

consider a being set such that

A31: f . k in a and

A32: a in A1 by A8, A16, A18, A21, NAT_1:13, TARSKI:def 4;

( a = p2 or a misses p2 ) by A7, A12, A22, A32;

then A33: A c= p0 by A8, A24, A28, A30, A31, A32, XBOOLE_0:3, ZFMISC_1:74;

consider B being set such that

A34: u in B and

A35: B in PB by A23, A26;

A36: ( p3 = B or p3 misses B ) by A23, A35, EQREL_1:def 4;

consider b being set such that

A37: u in b and

A38: b in B1 by A10, A24, A25, A28, A30, A33, TARSKI:def 4, XBOOLE_0:3;

( p3 = b or p3 misses b ) by A9, A13, A23, A38;

then B c= p0 by A10, A26, A34, A36, A37, A38, XBOOLE_0:3, ZFMISC_1:74;

hence f . (k + 1) in p0 by A26, A27, A34, A36, XBOOLE_0:3; :: thesis: verum

end;A22: p2 in PA and

A23: p3 in PB and

A24: f . k in p2 and

A25: u in p2 and

A26: u in p3 and

A27: f . (k + 1) in p3 by A4, A19;

consider A being set such that

A28: f . k in A and

A29: A in PA by A1, A11, A16, A18, A21, NAT_1:13, TARSKI:def 4;

A30: ( p2 = A or p2 misses A ) by A22, A29, EQREL_1:def 4;

consider a being set such that

A31: f . k in a and

A32: a in A1 by A8, A16, A18, A21, NAT_1:13, TARSKI:def 4;

( a = p2 or a misses p2 ) by A7, A12, A22, A32;

then A33: A c= p0 by A8, A24, A28, A30, A31, A32, XBOOLE_0:3, ZFMISC_1:74;

consider B being set such that

A34: u in B and

A35: B in PB by A23, A26;

A36: ( p3 = B or p3 misses B ) by A23, A35, EQREL_1:def 4;

consider b being set such that

A37: u in b and

A38: b in B1 by A10, A24, A25, A28, A30, A33, TARSKI:def 4, XBOOLE_0:3;

( p3 = b or p3 misses b ) by A9, A13, A23, A38;

then B c= p0 by A10, A26, A34, A36, A37, A38, XBOOLE_0:3, ZFMISC_1:74;

hence f . (k + 1) in p0 by A26, A27, A34, A36, XBOOLE_0:3; :: thesis: verum