let F be non empty FinSequence; for G being finite Function st rng G c= rng F holds
ex o being len F -element DoubleReorganization of dom G st
for n being Nat holds F . n = G . (o _ (n,1)) & ... & F . n = G . (o _ (n,(len (o . n))))
let G be finite Function; ( rng G c= rng F implies ex o being len F -element DoubleReorganization of dom G st
for n being Nat holds F . n = G . (o _ (n,1)) & ... & F . n = G . (o _ (n,(len (o . n)))) )
assume A1:
rng G c= rng F
; ex o being len F -element DoubleReorganization of dom G st
for n being Nat holds F . n = G . (o _ (n,1)) & ... & F . n = G . (o _ (n,(len (o . n))))
set D = dom G;
set d = the one-to-one onto FinSequence of dom G;
A2:
rng the one-to-one onto FinSequence of dom G = dom G
by FUNCT_2:def 3;
then A3:
card (dom the one-to-one onto FinSequence of dom G) = card (dom G)
by CARD_1:70;
A4:
dom the one-to-one onto FinSequence of dom G = Seg (len the one-to-one onto FinSequence of dom G)
by FINSEQ_1:def 3;
A5:
( card (dom G) = len the one-to-one onto FinSequence of dom G & card G = card (dom G) )
by CARD_1:62, A3;
defpred S1[ Nat] means ( $1 <= card G implies ex o being len F -element DoubleReorganization of the one-to-one onto FinSequence of dom G .: (Seg $1) st
for k being Nat holds F . k = G . (o _ (k,1)) & ... & F . k = G . (o _ (k,(len (o . k)))) );
A6:
S1[ 0 ]
A7:
for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be
Nat;
( S1[i] implies S1[i + 1] )
set i1 =
i + 1;
set di1 = the
one-to-one onto FinSequence of
dom G . (i + 1);
assume A8:
S1[
i]
;
S1[i + 1]
assume A9:
i + 1
<= card G
;
ex o being len F -element DoubleReorganization of the one-to-one onto FinSequence of dom G .: (Seg (i + 1)) st
for k being Nat holds F . k = G . (o _ (k,1)) & ... & F . k = G . (o _ (k,(len (o . k))))
then consider o being
len F -element DoubleReorganization of the
one-to-one onto FinSequence of
dom G .: (Seg i) such that A10:
for
j being
Nat holds
F . j = G . (o _ (j,1)) & ... &
F . j = G . (o _ (j,(len (o . j))))
by NAT_1:13, A8;
A11:
len o = len F
by CARD_1:def 7;
then A12:
dom o = dom F
by FINSEQ_3:29;
A13:
Values o = the
one-to-one onto FinSequence of
dom G .: (Seg i)
by Def7;
A14:
i + 1
in dom the
one-to-one onto FinSequence of
dom G
by NAT_1:11, A5, A9, FINSEQ_3:25;
then
the
one-to-one onto FinSequence of
dom G . (i + 1) in dom G
by A2, FUNCT_1:def 3;
then
G . ( the one-to-one onto FinSequence of dom G . (i + 1)) in rng G
by FUNCT_1:def 3;
then consider x being
object such that A15:
(
x in dom F &
F . x = G . ( the one-to-one onto FinSequence of dom G . (i + 1)) )
by A1, FUNCT_1:def 3;
reconsider x =
x as
Nat by A15;
set ox =
o . x;
set I1 =
<*( the one-to-one onto FinSequence of dom G . (i + 1))*>;
set oxI =
(o . x) ^ <*( the one-to-one onto FinSequence of dom G . (i + 1))*>;
A16:
i < i + 1
by NAT_1:13;
not the
one-to-one onto FinSequence of
dom G . (i + 1) in rng (o . x)
then A19:
(o . x) ^ <*( the one-to-one onto FinSequence of dom G . (i + 1))*> is
one-to-one
by GRAPHSP:1;
A20:
x in dom o
by A15, A11, FINSEQ_3:29;
o . x in rng o
by A15, A12, FUNCT_1:def 3;
then A21:
o . x is
FinSequence of the
one-to-one onto FinSequence of
dom G .: (Seg i)
by FINSEQ_1:def 11;
then A22:
rng (o . x) c= the
one-to-one onto FinSequence of
dom G .: (Seg i)
by FINSEQ_1:def 4;
A23:
(rng (o . x)) /\ ( the one-to-one onto FinSequence of dom G .: (Seg i)) = rng (o . x)
by A21, FINSEQ_1:def 4, XBOOLE_1:28;
not
i + 1
in Seg i
by A16, FINSEQ_1:1;
then
{(i + 1)} misses Seg i
by ZFMISC_1:52, ZFMISC_1:45;
then A24:
( the one-to-one onto FinSequence of dom G .: {(i + 1)}) /\ ( the one-to-one onto FinSequence of dom G .: (Seg i)) = the
one-to-one onto FinSequence of
dom G .: {}
by FUNCT_1:62;
then A25:
the
one-to-one onto FinSequence of
dom G .: {(i + 1)} misses the
one-to-one onto FinSequence of
dom G .: (Seg i)
;
Im ( the
one-to-one onto FinSequence of
dom G,
(i + 1))
= {( the one-to-one onto FinSequence of dom G . (i + 1))}
by A14, FUNCT_1:59;
then A26:
the
one-to-one onto FinSequence of
dom G .: {(i + 1)} = {( the one-to-one onto FinSequence of dom G . (i + 1))}
by RELAT_1:def 16;
A27:
rng <*( the one-to-one onto FinSequence of dom G . (i + 1))*> = {( the one-to-one onto FinSequence of dom G . (i + 1))}
by FINSEQ_1:39;
then
rng ((o . x) ^ <*( the one-to-one onto FinSequence of dom G . (i + 1))*>) = (rng (o . x)) \/ {( the one-to-one onto FinSequence of dom G . (i + 1))}
by FINSEQ_1:31;
then A28:
(rng ((o . x) ^ <*( the one-to-one onto FinSequence of dom G . (i + 1))*>)) /\ ( the one-to-one onto FinSequence of dom G .: (Seg i)) = (rng (o . x)) \/ {}
by A23, XBOOLE_1:23, A24, A26;
A29:
(Seg i) \/ {(i + 1)} = Seg (i + 1)
by FINSEQ_1:9;
then A30:
( the one-to-one onto FinSequence of dom G .: (Seg i)) \/ ( the one-to-one onto FinSequence of dom G .: {(i + 1)}) = the
one-to-one onto FinSequence of
dom G .: (Seg (i + 1))
by RELAT_1:120;
the
one-to-one onto FinSequence of
dom G .: (Seg i) c= the
one-to-one onto FinSequence of
dom G .: (Seg (i + 1))
by XBOOLE_1:7, A29, RELAT_1:123;
then A31:
rng (o . x) c= the
one-to-one onto FinSequence of
dom G .: (Seg (i + 1))
by A22;
set O =
o +* (
x,
((o . x) ^ <*( the one-to-one onto FinSequence of dom G . (i + 1))*>));
(rng ((o . x) ^ <*( the one-to-one onto FinSequence of dom G . (i + 1))*>)) \/ (( the one-to-one onto FinSequence of dom G .: (Seg i)) \ (rng (o . x))) =
((rng (o . x)) \/ {( the one-to-one onto FinSequence of dom G . (i + 1))}) \/ (( the one-to-one onto FinSequence of dom G .: (Seg i)) \ (rng (o . x)))
by A27, FINSEQ_1:31
.=
(rng (o . x)) \/ ({( the one-to-one onto FinSequence of dom G . (i + 1))} \/ (( the one-to-one onto FinSequence of dom G .: (Seg i)) \ (rng (o . x))))
by XBOOLE_1:4
.=
(rng (o . x)) \/ (({( the one-to-one onto FinSequence of dom G . (i + 1))} \/ ( the one-to-one onto FinSequence of dom G .: (Seg i))) \ (rng (o . x)))
by A22, A25, A26, XBOOLE_1:63, XBOOLE_1:87
.=
(rng (o . x)) \/ ({( the one-to-one onto FinSequence of dom G . (i + 1))} \/ ( the one-to-one onto FinSequence of dom G .: (Seg i)))
by XBOOLE_1:39
.=
the
one-to-one onto FinSequence of
dom G .: (Seg (i + 1))
by A26, A31, XBOOLE_1:12, A30
;
then reconsider O =
o +* (
x,
((o . x) ^ <*( the one-to-one onto FinSequence of dom G . (i + 1))*>)) as
len F -element DoubleReorganization of the
one-to-one onto FinSequence of
dom G .: (Seg (i + 1)) by A19, A20, Th37, A28;
take
O
;
for k being Nat holds F . k = G . (O _ (k,1)) & ... & F . k = G . (O _ (k,(len (O . k))))
let k be
Nat;
F . k = G . (O _ (k,1)) & ... & F . k = G . (O _ (k,(len (O . k))))
set Ok =
O . k;
A32:
(
dom <*( the one-to-one onto FinSequence of dom G . (i + 1))*> = Seg 1 &
Seg 1
= {1} &
<*( the one-to-one onto FinSequence of dom G . (i + 1))*> . 1
= the
one-to-one onto FinSequence of
dom G . (i + 1) )
by FINSEQ_1:38, FINSEQ_1:40, FINSEQ_1:2;
thus
F . k = G . (O _ (k,1)) & ... &
F . k = G . (O _ (k,(len (O . k))))
verumproof
let j be
Nat;
( not 1 <= j or not j <= len (O . k) or F . k = G . (O _ (k,j)) )
assume A33:
( 1
<= j &
j <= len (O . k) )
;
F . k = G . (O _ (k,j))
A34:
F . k = G . (o _ (k,1)) & ... &
F . k = G . (o _ (k,(len (o . k))))
by A10;
per cases
( k <> x or k = x )
;
suppose A36:
k = x
;
F . k = G . (O _ (k,j))then A37:
O . k = (o . x) ^ <*( the one-to-one onto FinSequence of dom G . (i + 1))*>
by A15, A12, FUNCT_7:31;
per cases
( j in dom (o . x) or not j in dom (o . x) )
;
suppose A38:
j in dom (o . x)
;
F . k = G . (O _ (k,j))then A39:
(
((o . x) ^ <*( the one-to-one onto FinSequence of dom G . (i + 1))*>) . j = (o . x) . j &
j <= len (o . x) )
by FINSEQ_1:def 7, FINSEQ_3:25;
o _ (
k,
j) =
((o . x) ^ <*( the one-to-one onto FinSequence of dom G . (i + 1))*>) . j
by A36, A38, FINSEQ_1:def 7
.=
(O . k) . j
by A36, A15, A12, FUNCT_7:31
;
hence
F . k = G . (O _ (k,j))
by A39, A36, A34, A33;
verum end; suppose
not
j in dom (o . x)
;
F . k = G . (O _ (k,j))then consider n being
Nat such that A40:
(
n in dom <*( the one-to-one onto FinSequence of dom G . (i + 1))*> &
j = (len (o . x)) + n )
by A37, A33, FINSEQ_3:25, FINSEQ_1:25;
n = 1
by A32, A40, TARSKI:def 1;
then F . k =
G . (((o . x) ^ <*( the one-to-one onto FinSequence of dom G . (i + 1))*>) . j)
by A40, A32, FINSEQ_1:def 7, A15, A36
.=
G . ((O . k) . j)
by A36, A15, A12, FUNCT_7:31
;
hence
F . k = G . (O _ (k,j))
;
verum end; end; end; end;
end;
end;
A41:
the one-to-one onto FinSequence of dom G .: (Seg (card (dom G))) = dom G
by A2, RELAT_1:113, A5, A4;
for i being Nat holds S1[i]
from NAT_1:sch 2(A6, A7);
then
ex o being len F -element DoubleReorganization of dom G st
for k being Nat holds F . k = G . (o _ (k,1)) & ... & F . k = G . (o _ (k,(len (o . k))))
by A41, A5;
hence
ex o being len F -element DoubleReorganization of dom G st
for n being Nat holds F . n = G . (o _ (n,1)) & ... & F . n = G . (o _ (n,(len (o . n))))
; verum