set N = { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ;
deffunc H1( Element of (Free (S,Y))) -> set = vf S;
A0: rng D is finite ;
A1: { H1(v) where v is Element of (Free (S,Y)) : v in rng D } is finite from FRAENKEL:sch 21(A0);
 A3: { (vf v) where v is Element of (Free (S,Y)) : v in rng D } is finite-membered
proof
let a be set ; :: according to FINSET_1:def 6 :: thesis: ( not a in { (vf v) where v is Element of (Free (S,Y)) : v in rng D } or a is finite )
assume a in { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ; :: thesis: a is finite
then ex v being Element of (Free (S,Y)) st
( a = H1(v) & v in rng D ) ;
hence a is finite ; :: thesis: verum
end;
deffunc H2( Element of dom B, set ) -> set = { the Element of (Y . (B . (S + 1))) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ Y)} \/ Y;
consider g being non empty FinSequence such that
A2: ( dom g = dom B & g . 1 = { the Element of (Y . (B . 1)) \ ((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V))} & ( for i, j being Element of dom B st j = i + 1 holds
g . j = H2(i,g . i) ) ) from MSAFREE5:sch 7();
 deffunc H3( Element of dom B, set ) -> set = union ((g . (S + 1)) \ (g . S));
consider f being non empty FinSequence such that
AA: ( dom f = dom B & f . 1 = union (g . 1) & ( for i, j being Element of dom B st j = i + 1 holds
f . j = H3(i,f . i) ) ) from MSAFREE5:sch 7();
 defpred S1[ Nat] means ( S in dom B implies g . S is finite );
B1: S1[1] by A2;
B2: for i being Nat st i >= 1 & S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( i >= 1 & S1[i] implies S1[i + 1] )
assume B4: ( i >= 1 & S1[i] & i + 1 in dom B ) ; :: thesis: g . (i + 1) is finite
then ( i <= i + 1 & i + 1 <= len B ) by NAT_1:12, FINSEQ_3:25;
then i <= len B by XXREAL_0:2;
then reconsider i = i as Element of dom B by B4, FINSEQ_3:25;
( g . (i + 1) = H2(i,g . i) & g . i is finite ) by B4, A2;
hence g . (i + 1) is finite ; :: thesis: verum
end;
B3: for i being Nat st i >= 1 holds
S1[i] from NAT_1:sch 8(B1, B2);
 defpred S2[ Nat] means ( S + 1 in dom B implies ( g . (S + 1) = {(f . (S + 1))} \/ (g . S) & f . (S + 1) nin g . S & f . (S + 1) = the Element of (Y . (B . (S + 1))) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ (g . S)) ) );
C1: S2[1]
proof
assume C2: 1 + 1 in dom B ; :: thesis: ( g . (1 + 1) = {(f . (1 + 1))} \/ (g . 1) & f . (1 + 1) nin g . 1 & f . (1 + 1) = the Element of (Y . (B . (1 + 1))) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ (g . 1)) )
then 1 + 1 <= len B by FINSEQ_3:25;
then 1 <= len B by XXREAL_0:2;
then reconsider i = 1, j = 1 + 1 as Element of dom B by C2, FINSEQ_3:25;
reconsider gi = g . i as finite set by A2;
set x = the Element of (Y . (B . j)) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ gi);
C6: the Element of (Y . (B . j)) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ gi) nin ((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ gi by A1, A3, XBOOLE_0:def 5;
then C3: the Element of (Y . (B . j)) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ gi) nin g . i by XBOOLE_0:def 3;
( g . 2 = H2(i,g . 1) & H2(i,g . 1) = { the Element of (Y . (B . j)) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ gi)} \/ (g . 1) & f . 2 = H3(i,f . 1) & H3(i,f . 1) = union ((g . (i + 1)) \ (g . i)) ) by A2, AA, C2;
then ( f . 2 = union { the Element of (Y . (B . j)) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ gi)} & union { the Element of (Y . (B . j)) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ gi)} = the Element of (Y . (B . j)) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ gi) ) by C3, EXCHSORT:3;
hence ( g . (1 + 1) = {(f . (1 + 1))} \/ (g . 1) & f . (1 + 1) nin g . 1 & f . (1 + 1) = the Element of (Y . (B . (1 + 1))) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ (g . 1)) ) by C6, A2, XBOOLE_0:def 3; :: thesis: verum
end;
C5: for i being Nat st i >= 1 & S2[i] holds
S2[i + 1]
proof
let i be Nat; :: thesis: ( i >= 1 & S2[i] implies S2[i + 1] )
assume Z0: i >= 1 ; :: thesis: ( not S2[i] or S2[i + 1] )
assume S2[i] ; :: thesis: S2[i + 1]
assume Z2: (i + 1) + 1 in dom B ; :: thesis: ( g . ((i + 1) + 1) = {(f . ((i + 1) + 1))} \/ (g . (i + 1)) & f . ((i + 1) + 1) nin g . (i + 1) & f . ((i + 1) + 1) = the Element of (Y . (B . ((i + 1) + 1))) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ (g . (i + 1))) )
then ( i + 1 <= (i + 1) + 1 & (i + 1) + 1 <= len B ) by NAT_1:12, FINSEQ_3:25;
then C6: ( 1 <= i + 1 & i + 1 <= len B ) by NAT_1:12, XXREAL_0:2;
then reconsider j2 = (i + 1) + 1, j = 1 + i as Element of dom B by Z2, FINSEQ_3:25;
i <= i + 1 by NAT_1:12;
then i <= len B by C6, XXREAL_0:2;
then i in dom B by Z0, FINSEQ_3:25;
then reconsider gi = g . i, gj = g . j as finite set by B3, FINSEQ_3:25;
set x = the Element of (Y . (B . j2)) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ gj);
C7: the Element of (Y . (B . j2)) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ gj) nin ((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ gj by A1, A3, XBOOLE_0:def 5;
then C3: the Element of (Y . (B . j2)) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ gj) nin g . j by XBOOLE_0:def 3;
( g . j2 = H2(j,g . j) & H2(j,g . j) = { the Element of (Y . (B . j2)) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ gj)} \/ (g . j) & f . j2 = H3(j,f . j) & H3(j,f . j) = union ((g . (j + 1)) \ (g . j)) ) by A2, AA;
then ( f . j2 = union { the Element of (Y . (B . j2)) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ gj)} & union { the Element of (Y . (B . j2)) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ gj)} = the Element of (Y . (B . j2)) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ gj) ) by C3, EXCHSORT:3;
hence ( g . ((i + 1) + 1) = {(f . ((i + 1) + 1))} \/ (g . (i + 1)) & f . ((i + 1) + 1) nin g . (i + 1) & f . ((i + 1) + 1) = the Element of (Y . (B . ((i + 1) + 1))) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ (g . (i + 1))) ) by C7, A2, XBOOLE_0:def 3; :: thesis: verum
end;
C7: for i being Nat st i >= 1 holds
S2[i] from NAT_1:sch 8(C1, C5);
C6: now :: thesis: for i being Element of dom B st i + 1 in dom B holds
( g . (i + 1) = {(f . (i + 1))} \/ (g . i) & f . (i + 1) nin g . i & f . (i + 1) = the Element of (Y . (B . (i + 1))) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ (g . i)) )
let i be Element of dom B; :: thesis: ( i + 1 in dom B implies ( g . (i + 1) = {(f . (i + 1))} \/ (g . i) & f . (i + 1) nin g . i & f . (i + 1) = the Element of (Y . (B . (i + 1))) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ (g . i)) ) )
i >= 1 by FINSEQ_3:25;
hence ( i + 1 in dom B implies ( g . (i + 1) = {(f . (i + 1))} \/ (g . i) & f . (i + 1) nin g . i & f . (i + 1) = the Element of (Y . (B . (i + 1))) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ (g . i)) ) ) by C7; :: thesis: verum
end;
rng f c= Union Y
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng f or a in Union Y )
assume a in rng f ; :: thesis: a in Union Y
then consider b being object such that
A5: ( b in dom f & a = f . b ) by FUNCT_1:def 3;
reconsider b = b as Element of dom B by AA, A5;
b >= 1 by FINSEQ_3:25;
per cases then ( b = 1 or b > 1 ) by XXREAL_0:1;
suppose b = 1 ; :: thesis: a in Union Y
then ( a in Y . (B . b) & B . b in the carrier of S & the carrier of S = dom Y ) by A1, A2, A3, AA, A5, XBOOLE_0:def 5, PARTFUN1:def 2;
hence a in Union Y by CARD_5:2; :: thesis: verum
end;
suppose b > 1 ; :: thesis: a in Union Y
then b >= 1 + 1 by NAT_1:13;
then consider c being Nat such that
D1: b = (1 + 1) + c by NAT_1:10;
D2: b = (1 + c) + 1 by D1;
then ( len B >= b & b > 1 + c ) by NAT_1:13, FINSEQ_3:25;
then ( len B >= 1 + c & 1 + c >= 1 ) by NAT_1:12, XXREAL_0:2;
then reconsider c1 = 1 + c as Element of dom B by FINSEQ_3:25;
g . c1 is finite by B3, FINSEQ_3:25;
then ( a = the Element of (Y . (B . b)) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ (g . c1)) & (Y . (B . b)) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ (g . c1)) <> {} ) by C6, A1, A3, D2, A5;
then ( a in Y . (B . b) & B . b in the carrier of S & the carrier of S = dom Y ) by XBOOLE_0:def 5, PARTFUN1:def 2;
hence a in Union Y by CARD_5:2; :: thesis: verum
end;
end;
end;
then reconsider f = f as FinSequence of Union Y by FINSEQ_1:def 4;
E0: for i, j being Element of dom B st i <= j holds
g . i c= g . j
proof
let i, j be Element of dom B; :: thesis: ( i <= j implies g . i c= g . j )
defpred S3[ Nat] means ( S in dom B implies g . i c= g . S );
E1: S3[i] ;
E2: for j being Nat st j >= i & S3[j] holds
S3[j + 1]
proof
let j be Nat; :: thesis: ( j >= i & S3[j] implies S3[j + 1] )
assume E3: ( j >= i & S3[j] & j + 1 in dom B ) ; :: thesis: g . i c= g . (j + 1)
then ( len B >= j + 1 & j + 1 >= j & i >= 1 ) by NAT_1:12, FINSEQ_3:25;
then E4: ( len B >= j & j >= 1 ) by E3, XXREAL_0:2;
then j in dom B by FINSEQ_3:25;
then g . (j + 1) = {(f . (j + 1))} \/ (g . j) by C6, E3;
then ( g . i c= g . j & g . j c= g . (j + 1) ) by E3, E4, XBOOLE_1:7, FINSEQ_3:25;
hence g . i c= g . (j + 1) ; :: thesis: verum
end;
for j being Nat st j >= i holds
S3[j] from NAT_1:sch 8(E1, E2);
 hence ( i <= j implies g . i c= g . j ) ; :: thesis: verum
end;
F0: for i, j being Element of dom B st i < j holds
( f . j nin g . i & f . j in g . j )
proof
let i, j be Element of dom B; :: thesis: ( i < j implies ( f . j nin g . i & f . j in g . j ) )
assume i < j ; :: thesis: ( f . j nin g . i & f . j in g . j )
then i + 1 <= j by NAT_1:13;
then consider k being Nat such that
E5: j = (i + 1) + k by NAT_1:10;
E6: j = (i + k) + 1 by E5;
len B >= (i + k) + 1 by E5, FINSEQ_3:25;
then ( len B > i + k & i + k >= i & i >= 1 ) by NAT_1:12, NAT_1:13, FINSEQ_3:25;
then ( len B >= i + k & i + k >= 1 ) by XXREAL_0:2;
then reconsider ik = i + k as Element of dom B by FINSEQ_3:25;
( g . i c= g . ik & f . j nin g . ik & g . j = {(f . j)} \/ (g . ik) ) by C6, E6, E0, NAT_1:12;
hence ( f . j nin g . i & f . j in g . j ) by ZFMISC_1:136; :: thesis: verum
end;
F1: for b being Element of dom B holds f . b in g . b
proof
let b be Element of dom B; :: thesis: f . b in g . b
b >= 1 by FINSEQ_3:25;
per cases then ( b = 1 or b > 1 ) by XXREAL_0:1;
suppose b = 1 ; :: thesis: f . b in g . b
hence f . b in g . b by AA, A2, TARSKI:def 1; :: thesis: verum
end;
suppose D0: b > 1 ; :: thesis: f . b in g . b
b <= len B by FINSEQ_3:25;
then 1 <= len B by D0, XXREAL_0:2;
then reconsider c1 = 1 as Element of dom B by FINSEQ_3:25;
c1 < b by D0;
hence f . b in g . b by F0; :: thesis: verum
end;
end;
end;
f is B -sorts
proof
thus dom f = dom B by AA; :: according to MSAFREE5:def 36 :: thesis: for i being Nat st i in dom B holds
f . i in Y . (B . i)
let i be Nat; :: thesis: ( i in dom B implies f . i in Y . (B . i) )
assume i in dom B ; :: thesis: f . i in Y . (B . i)
then reconsider j = i as Element of dom B ;
j >= 1 by FINSEQ_3:25;
per cases then ( i = 1 or i > 1 ) by XXREAL_0:1;
suppose i = 1 ; :: thesis: f . i in Y . (B . i)
then ( f . i = union { the Element of (Y . (B . j)) \ ((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V))} & (Y . (B . j)) \ ((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) <> {} ) by AA, A1, A2, A3;
hence f . i in Y . (B . i) by XBOOLE_0:def 5; :: thesis: verum
end;
suppose i > 1 ; :: thesis: f . i in Y . (B . i)
then i >= 1 + 1 by NAT_1:13;
then consider c being Nat such that
D1: i = (1 + 1) + c by NAT_1:10;
D2: j = (1 + c) + 1 by D1;
then ( len B >= j & j > 1 + c ) by NAT_1:13, FINSEQ_3:25;
then ( len B >= 1 + c & 1 + c >= 1 ) by NAT_1:12, XXREAL_0:2;
then reconsider c1 = 1 + c as Element of dom B by FINSEQ_3:25;
g . c1 is finite by B3, FINSEQ_3:25;
then ( f . j = the Element of (Y . (B . j)) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ (g . c1)) & (Y . (B . j)) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ (g . c1)) <> {} ) by C6, A1, A3, D2;
hence f . i in Y . (B . i) by XBOOLE_0:def 5; :: thesis: verum
end;
end;
end;
then reconsider f = f as B -sorts FinSequence of Union Y ;
take f ; :: thesis: ( f is one-to-one & f is V -omitting & f is D -omitting )
thus f is one-to-one :: thesis: ( f is V -omitting & f is D -omitting )
proof
let a be object ; :: according to FUNCT_1:def 4 :: thesis: for b1 being object holds
( not a in proj1 f or not b1 in proj1 f or not f . a = f . b1 or a = b1 )
let b be object ; :: thesis: ( not a in proj1 f or not b in proj1 f or not f . a = f . b or a = b )
assume F2: ( a in dom f & b in dom f & f . a = f . b & a <> b ) ; :: thesis: contradiction
then reconsider a = a, b = b as Element of dom B by AA;
( a < b or b < a ) by F2, XXREAL_0:1;
then ( ( f . b in g . a & f . b nin g . a ) or ( f . a in g . b & f . a nin g . b ) ) by F0, F1, F2;
hence contradiction ; :: thesis: verum
end;
now :: thesis: for a being object st a in rng f holds
a nin (union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)
let a be object ; :: thesis: ( a in rng f implies b1 nin (union { (vf b2) where v is Element of (Free (S,Y)) : b2 in rng D } ) \/ (rng V) )
assume a in rng f ; :: thesis: b1 nin (union { (vf b2) where v is Element of (Free (S,Y)) : b2 in rng D } ) \/ (rng V)
then consider b being object such that
A5: ( b in dom f & a = f . b ) by FUNCT_1:def 3;
reconsider b = b as Element of dom B by AA, A5;
1 <= b by FINSEQ_3:25;
per cases then ( b = 1 or b > 1 ) by XXREAL_0:1;
suppose b = 1 ; :: thesis: b1 nin (union { (vf b2) where v is Element of (Free (S,Y)) : b2 in rng D } ) \/ (rng V)
then ( a = union { the Element of (Y . (B . b)) \ ((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V))} & (Y . (B . b)) \ ((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) <> {} ) by AA, A1, A2, A3, A5;
hence a nin (union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V) by XBOOLE_0:def 5; :: thesis: verum
end;
suppose b > 1 ; :: thesis: b1 nin (union { (vf b2) where v is Element of (Free (S,Y)) : b2 in rng D } ) \/ (rng V)
then b >= 1 + 1 by NAT_1:13;
then consider c being Nat such that
D1: b = (1 + 1) + c by NAT_1:10;
D2: b = (1 + c) + 1 by D1;
then ( len B >= b & b > 1 + c ) by NAT_1:13, FINSEQ_3:25;
then ( len B >= 1 + c & 1 + c >= 1 ) by NAT_1:12, XXREAL_0:2;
then reconsider c1 = 1 + c as Element of dom B by FINSEQ_3:25;
g . c1 is finite by B3, FINSEQ_3:25;
then ( a = the Element of (Y . (B . b)) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ (g . c1)) & (Y . (B . b)) \ (((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ (g . c1)) <> {} ) by C6, A1, A3, D2, A5;
then a nin ((union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V)) \/ (g . c1) by XBOOLE_0:def 5;
hence a nin (union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V) by XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
then A4: rng f misses (union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ) \/ (rng V) by XBOOLE_0:3;
thus rng V misses rng f by A4, XBOOLE_1:7, XBOOLE_1:63; :: according to MSAFREE5:def 39 :: thesis: f is D -omitting
let t be Element of (Free (S,Y)); :: according to MSAFREE5:def 41 :: thesis: ( t in rng D implies vf t misses rng f )
assume t in rng D ; :: thesis: vf t misses rng f
then vf t in { (vf v) where v is Element of (Free (S,Y)) : v in rng D } ;
then vf t c= union { (vf v) where v is Element of (Free (S,Y)) : v in rng D } by ZFMISC_1:74;
hence vf t misses rng f by A4, XBOOLE_1:10, XBOOLE_1:63; :: thesis: verum