let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let F be Finite_Sep_Sequence of S; :: thesis:
defpred S₁[ Nat] means for F being Finite_Sep_Sequence of S st len F = $1 holds
ex G being Finite_Sep_Sequence of S st
( union (rng F) = union (rng G) & ( for n being Nat st n in dom G holds
( G . n <> {} & ex m being Nat st
( m in dom F & F . m = G . n ) ) ) );
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis:
assume A2: S₁[n] ; :: thesis:
let F be Finite_Sep_Sequence of S; :: thesis:
assume A3: len F = n + 1 ; :: thesis:
reconsider n = n as Element of NAT by ORDINAL1:def 12;
reconsider F1 = F | (Seg n) as Finite_Sep_Sequence of S by MESFUNC2:33;
A4: n <= len F by A3, NAT_1:11;
then A5: len F1 = n by FINSEQ_1:17;
then consider G1 being Finite_Sep_Sequence of S such that
A6: union (rng F1) = union (rng G1) and
A7: for n being Nat st n in dom G1 holds
( G1 . n <> {} & ex m being Nat st
( m in dom F1 & F1 . m = G1 . n ) ) by A2;
A8: ( dom F = dom (F1 ^ <*(F . (n + 1))*>) & ( for k being Nat st k in dom F holds
F . k = (F1 ^ <*(F . (n + 1))*>) . k ) )

proof

thus dom (F1 ^ <*(F . (n + 1))*>) = Seg ((len F1) + (len <*(F . (n + 1))*>)) by FINSEQ_1:def 7
.= Seg (n + 1) by A5, FINSEQ_1:39
.= dom F by A3, FINSEQ_1:def 3 ; :: thesis:
let k be Nat; :: thesis:
assume A9: k in dom F ; :: thesis:

now :: thesis:

per cases ;

case A10: k in dom F1 ; :: thesis:

then k in Seg n by A4, FINSEQ_1:17;
then k <= n by FINSEQ_1:1;
then A11: (F | n) . k = F . k by FINSEQ_3:112;
(F1 ^ <*(F . (n + 1))*>) . k = F1 . k by A10, FINSEQ_1:def 7;
hence F . k = (F1 ^ <*(F . (n + 1))*>) . k by A11, FINSEQ_1:def 15; :: thesis:

end;

case A12: not k in dom F1 ; :: thesis:

A13: k in Seg (n + 1) by A3, A9, FINSEQ_1:def 3;
not k in Seg n by A4, A12, FINSEQ_1:17;
then ( not 1 <= k or not k <= n ) by FINSEQ_1:1;
then A14: not k < n + 1 by A13, FINSEQ_1:1, NAT_1:13;
dom <*(F . (n + 1))*> = Seg 1 by FINSEQ_1:def 8;
then A15: 1 in dom <*(F . (n + 1))*> by FINSEQ_1:2, TARSKI:def 1;
A16: k <= n + 1 by A13, FINSEQ_1:1;
then (F1 ^ <*(F . (n + 1))*>) . k = (F1 ^ <*(F . (n + 1))*>) . ((len F1) + 1) by A5, A14, XXREAL_0:1
.= <*(F . (n + 1))*> . 1 by A15, FINSEQ_1:def 7
.= F . (n + 1) by FINSEQ_1:def 8 ;
hence F . k = (F1 ^ <*(F . (n + 1))*>) . k by A14, A16, XXREAL_0:1; :: thesis:

end;

hence F . k = (F1 ^ <*(F . (n + 1))*>) . k ; :: thesis:

end;

then A17: F = F1 ^ <*(F . (n + 1))*> by FINSEQ_1:13;
ex G being Finite_Sep_Sequence of S st
( union (rng F) = union (rng G) & ( for k being Nat st k in dom G holds
( G . k <> {} & ex m being Nat st
( m in dom F & F . m = G . k ) ) ) )

proof

now :: thesis:

per cases ;

case F . (n + 1) = {} ; :: thesis:

then A18: rng <*(F . (n + 1))*> = {{}} by FINSEQ_1:38;
take G = G1; :: thesis:
A19: for k being Nat st k in dom G holds
( G . k <> {} & ex m being Nat st
( m in dom F & F . m = G . k ) )

proof

let k be Nat; :: thesis:
A20: dom F1 c= dom F by A8, FINSEQ_1:26;
assume A21: k in dom G ; :: thesis:
then consider m being Nat such that
A22: m in dom F1 and
A23: F1 . m = G . k by A7;
F1 . m = F . m by A17, A22, FINSEQ_1:def 7;
hence ( G . k <> {} & ex m being Nat st
( m in dom F & F . m = G . k ) ) by A7, A21, A22, A23, A20; :: thesis:

end;

rng F = (rng F1) \/ (rng <*(F . (n + 1))*>) by A17, FINSEQ_1:31;
then union (rng F) = (union (rng F1)) \/ (union (rng <*(F . (n + 1))*>)) by ZFMISC_1:78
.= (union (rng F1)) \/ {} by A18, ZFMISC_1:25
.= union (rng G) by A6 ;
hence ex G being Finite_Sep_Sequence of S st
( union (rng F) = union (rng G) & ( for k being Nat st k in dom G holds
( G . k <> {} & ex m being Nat st
( m in dom F & F . m = G . k ) ) ) ) by A19; :: thesis:

end;

case A24: F . (n + 1) <> {} ; :: thesis:

A25: for k, m being object st k <> m holds
(G1 ^ <*(F . (n + 1))*>) . k misses (G1 ^ <*(F . (n + 1))*>) . m

proof

let k, m be object ; :: thesis:
assume A26: k <> m ; :: thesis:

now :: thesis:

per cases ;

case A27: ( k in dom (G1 ^ <*(F . (n + 1))*>) & m in dom (G1 ^ <*(F . (n + 1))*>) ) ; :: thesis:

then reconsider k = k, m = m as Element of NAT ;

now :: thesis:

per cases ;

case k = len (G1 ^ <*(F . (n + 1))*>) ; :: thesis:

then k = (len G1) + (len <*(F . (n + 1))*>) by FINSEQ_1:22;
then A28: k = (len G1) + 1 by FINSEQ_1:39;
1 <= len <*(F . (n + 1))*> by FINSEQ_1:39;
then A29: (G1 ^ <*(F . (n + 1))*>) . k = <*(F . (n + 1))*> . 1 by A28, FINSEQ_1:65
.= F . (n + 1) by FINSEQ_1:def 8 ;
A30: m in Seg (len (G1 ^ <*(F . (n + 1))*>)) by A27, FINSEQ_1:def 3;
then m in Seg ((len G1) + (len <*(F . (n + 1))*>)) by FINSEQ_1:22;
then m in Seg ((len G1) + 1) by FINSEQ_1:39;
then m <= (len G1) + 1 by FINSEQ_1:1;
then m < (len G1) + 1 by A26, A28, XXREAL_0:1;
then A31: m <= len G1 by NAT_1:13;
1 <= m by A30, FINSEQ_1:1;
then A32: m in dom G1 by A31, FINSEQ_3:25;
then consider m1 being Nat such that
A33: m1 in dom F1 and
A34: F1 . m1 = G1 . m by A7;
m1 in Seg (len F1) by A33, FINSEQ_1:def 3;
then m1 <= n by A5, FINSEQ_1:1;
then A35: m1 <> n + 1 by NAT_1:13;
(G1 ^ <*(F . (n + 1))*>) . m = G1 . m by A32, FINSEQ_1:def 7;
then (G1 ^ <*(F . (n + 1))*>) . m = F . m1 by A17, A33, A34, FINSEQ_1:def 7;
hence (G1 ^ <*(F . (n + 1))*>) . k misses (G1 ^ <*(F . (n + 1))*>) . m by A29, A35, PROB_2:def 2; :: thesis:

end;

case k <> len (G1 ^ <*(F . (n + 1))*>) ; :: thesis:

then k <> (len G1) + (len <*(F . (n + 1))*>) by FINSEQ_1:22;
then A36: k <> (len G1) + 1 by FINSEQ_1:39;
A37: k in Seg (len (G1 ^ <*(F . (n + 1))*>)) by A27, FINSEQ_1:def 3;
then k in Seg ((len G1) + (len <*(F . (n + 1))*>)) by FINSEQ_1:22;
then k in Seg ((len G1) + 1) by FINSEQ_1:39;
then k <= (len G1) + 1 by FINSEQ_1:1;
then k < (len G1) + 1 by A36, XXREAL_0:1;
then A38: k <= len G1 by NAT_1:13;
1 <= k by A37, FINSEQ_1:1;
then A39: k in dom G1 by A38, FINSEQ_3:25;
then A40: (G1 ^ <*(F . (n + 1))*>) . k = G1 . k by FINSEQ_1:def 7;

now :: thesis:

per cases ;

case m = len (G1 ^ <*(F . (n + 1))*>) ; :: thesis:

then m = (len G1) + (len <*(F . (n + 1))*>) by FINSEQ_1:22;
then A41: m = (len G1) + 1 by FINSEQ_1:39;
1 <= len <*(F . (n + 1))*> by FINSEQ_1:39;
then A42: (G1 ^ <*(F . (n + 1))*>) . m = <*(F . (n + 1))*> . 1 by A41, FINSEQ_1:65
.= F . (n + 1) by FINSEQ_1:def 8 ;
consider k1 being Nat such that
A43: k1 in dom F1 and
A44: F1 . k1 = G1 . k by A7, A39;
k1 in Seg (len F1) by A43, FINSEQ_1:def 3;
then k1 <= n by A5, FINSEQ_1:1;
then A45: k1 <> n + 1 by NAT_1:13;
(G1 ^ <*(F . (n + 1))*>) . k = F . k1 by A17, A40, A43, A44, FINSEQ_1:def 7;
hence (G1 ^ <*(F . (n + 1))*>) . k misses (G1 ^ <*(F . (n + 1))*>) . m by A42, A45, PROB_2:def 2; :: thesis:

end;

case m <> len (G1 ^ <*(F . (n + 1))*>) ; :: thesis:

then m <> (len G1) + (len <*(F . (n + 1))*>) by FINSEQ_1:22;
then A46: m <> (len G1) + 1 by FINSEQ_1:39;
A47: m in Seg (len (G1 ^ <*(F . (n + 1))*>)) by A27, FINSEQ_1:def 3;
then m in Seg ((len G1) + (len <*(F . (n + 1))*>)) by FINSEQ_1:22;
then m in Seg ((len G1) + 1) by FINSEQ_1:39;
then m <= (len G1) + 1 by FINSEQ_1:1;
then m < (len G1) + 1 by A46, XXREAL_0:1;
then A48: m <= len G1 by NAT_1:13;
1 <= m by A47, FINSEQ_1:1;
then m in dom G1 by A48, FINSEQ_3:25;
then (G1 ^ <*(F . (n + 1))*>) . m = G1 . m by FINSEQ_1:def 7;
hence (G1 ^ <*(F . (n + 1))*>) . k misses (G1 ^ <*(F . (n + 1))*>) . m by A26, A40, PROB_2:def 2; :: thesis:

end;

hence (G1 ^ <*(F . (n + 1))*>) . k misses (G1 ^ <*(F . (n + 1))*>) . m ; :: thesis:

end;

hence (G1 ^ <*(F . (n + 1))*>) . k misses (G1 ^ <*(F . (n + 1))*>) . m ; :: thesis:

end;

case ( not k in dom (G1 ^ <*(F . (n + 1))*>) or not m in dom (G1 ^ <*(F . (n + 1))*>) ) ; :: thesis:

then ( (G1 ^ <*(F . (n + 1))*>) . k = {} or (G1 ^ <*(F . (n + 1))*>) . m = {} ) by FUNCT_1:def 2;
hence (G1 ^ <*(F . (n + 1))*>) . k misses (G1 ^ <*(F . (n + 1))*>) . m ; :: thesis:

end;

hence (G1 ^ <*(F . (n + 1))*>) . k misses (G1 ^ <*(F . (n + 1))*>) . m ; :: thesis:

end;

1 <= n + 1 by NAT_1:11;
then n + 1 in Seg (n + 1) by FINSEQ_1:1;
then n + 1 in dom F by A3, FINSEQ_1:def 3;
then F . (n + 1) in rng F by FUNCT_1:3;
then <*(F . (n + 1))*> is FinSequence of S by FINSEQ_1:74;
then reconsider G = G1 ^ <*(F . (n + 1))*> as Finite_Sep_Sequence of S by A25, FINSEQ_1:75, PROB_2:def 2;
A49: len G = (len G1) + (len <*(F . (n + 1))*>) by FINSEQ_1:22
.= (len G1) + 1 by FINSEQ_1:39 ;
A50: for k being Nat st k in dom G holds
( G . k <> {} & ex m being Nat st
( m in dom F & F . m = G . k ) )

proof

let k be Nat; :: thesis:
assume A51: k in dom G ; :: thesis:
reconsider k = k as Element of NAT by ORDINAL1:def 12;

now :: thesis:

per cases ;

case A52: k = len G ; :: thesis:

1 <= n + 1 by NAT_1:11;
then n + 1 in Seg (n + 1) by FINSEQ_1:1;
then A53: n + 1 in dom F by A3, FINSEQ_1:def 3;
dom <*(F . (n + 1))*> = Seg 1 by FINSEQ_1:38;
then 1 in dom <*(F . (n + 1))*> by FINSEQ_1:2, TARSKI:def 1;
then G . k = <*(F . (n + 1))*> . 1 by A49, A52, FINSEQ_1:def 7
.= F . (n + 1) by FINSEQ_1:def 8 ;
hence ( G . k <> {} & ex m being Nat st
( m in dom F & F . m = G . k ) ) by A24, A53; :: thesis:

end;

case A54: k <> len G ; :: thesis:

k <= len G by A51, FINSEQ_3:25;
then k < len G by A54, XXREAL_0:1;
then A55: k <= len G1 by A49, NAT_1:13;
1 <= k by A51, FINSEQ_3:25;
then A56: k in dom G1 by A55, FINSEQ_3:25;
then A57: G . k = G1 . k by FINSEQ_1:def 7;
ex m being Nat st
( m in dom F & F . m = G . k )

proof

consider m being Nat such that
A58: ( m in dom F1 & F1 . m = G1 . k ) by A7, A56;
take m ; :: thesis:
dom F1 c= dom F by A8, FINSEQ_1:26;
hence ( m in dom F & F . m = G . k ) by A17, A57, A58, FINSEQ_1:def 7; :: thesis:

end;

hence ( G . k <> {} & ex m being Nat st
( m in dom F & F . m = G . k ) ) by A7, A56, A57; :: thesis:

end;

hence ( G . k <> {} & ex m being Nat st
( m in dom F & F . m = G . k ) ) ; :: thesis:

end;

take G = G; :: thesis:
rng F = (rng F1) \/ (rng <*(F . (n + 1))*>) by A17, FINSEQ_1:31;
then union (rng F) = (union (rng F1)) \/ (union (rng <*(F . (n + 1))*>)) by ZFMISC_1:78
.= union ((rng G1) \/ (rng <*(F . (n + 1))*>)) by A6, ZFMISC_1:78
.= union (rng G) by FINSEQ_1:31 ;
hence ex G being Finite_Sep_Sequence of S st
( union (rng F) = union (rng G) & ( for k being Nat st k in dom G holds
( G . k <> {} & ex m being Nat st
( m in dom F & F . m = G . k ) ) ) ) by A50; :: thesis:

end;

hence ex G being Finite_Sep_Sequence of S st
( union (rng F) = union (rng G) & ( for k being Nat st k in dom G holds
( G . k <> {} & ex m being Nat st
( m in dom F & F . m = G . k ) ) ) ) ; :: thesis:

end;

hence ex G being Finite_Sep_Sequence of S st
( union (rng F) = union (rng G) & ( for n being Nat st n in dom G holds
( G . n <> {} & ex m being Nat st
( m in dom F & F . m = G . n ) ) ) ) ; :: thesis:

end;

A59: len F = len F ;
A60: S₁[ 0 ]

proof

let F be Finite_Sep_Sequence of S; :: thesis:
assume A61: len F = 0 ; :: thesis:
take G = F; :: thesis:
G = {} by A61;
hence ( union (rng F) = union (rng G) & ( for n being Nat st n in dom G holds
( G . n <> {} & ex m being Nat st
( m in dom F & F . m = G . n ) ) ) ) ; :: thesis:

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A60, A1);
hence ex G being Finite_Sep_Sequence of S st
( union (rng F) = union (rng G) & ( for n being Nat st n in dom G holds
( G . n <> {} & ex m being Nat st
( m in dom F & F . m = G . n ) ) ) ) by A59; :: thesis: