let i be Nat; for D being finite set
for o being DoubleReorganization of D
for F being one-to-one FinSequence st i in dom o & (rng F) /\ D c= rng (o . i) holds
o +* (i,F) is DoubleReorganization of (rng F) \/ (D \ (rng (o . i)))
let D be finite set ; for o being DoubleReorganization of D
for F being one-to-one FinSequence st i in dom o & (rng F) /\ D c= rng (o . i) holds
o +* (i,F) is DoubleReorganization of (rng F) \/ (D \ (rng (o . i)))
let o be DoubleReorganization of D; for F being one-to-one FinSequence st i in dom o & (rng F) /\ D c= rng (o . i) holds
o +* (i,F) is DoubleReorganization of (rng F) \/ (D \ (rng (o . i)))
let F be one-to-one FinSequence; ( i in dom o & (rng F) /\ D c= rng (o . i) implies o +* (i,F) is DoubleReorganization of (rng F) \/ (D \ (rng (o . i))) )
assume A1:
( i in dom o & (rng F) /\ D c= rng (o . i) )
; o +* (i,F) is DoubleReorganization of (rng F) \/ (D \ (rng (o . i)))
set rF = rng F;
set oi = o . i;
set roi = rng (o . i);
set oF = o +* (i,F);
A2:
dom (o +* (i,F)) = dom o
by FUNCT_7:30;
A3:
(o +* (i,F)) . i = F
by A1, FUNCT_7:31;
A4:
Values o = D
by Def7;
rng (o +* (i,F)) c= ((rng F) \/ (D \ (rng (o . i)))) *
proof
let y be
object ;
TARSKI:def 3 ( not y in rng (o +* (i,F)) or y in ((rng F) \/ (D \ (rng (o . i)))) * )
assume
y in rng (o +* (i,F))
;
y in ((rng F) \/ (D \ (rng (o . i)))) *
then consider x being
object such that A5:
(
x in dom (o +* (i,F)) &
(o +* (i,F)) . x = y )
by FUNCT_1:def 3;
per cases
( x = i or x <> i )
;
suppose A7:
x <> i
;
y in ((rng F) \/ (D \ (rng (o . i)))) * then A8:
(o +* (i,F)) . x = o . x
by FUNCT_7:32;
o . x in rng o
by A2, A5, FUNCT_1:def 3;
then reconsider ox =
o . x as
FinSequence of
D by FINSEQ_1:def 11;
rng ox misses rng (o . i)
proof
assume
rng ox meets rng (o . i)
;
contradiction
then consider z being
object such that A9:
(
z in rng ox &
z in rng (o . i) )
by XBOOLE_0:3;
consider a being
object such that A10:
(
a in dom ox &
ox . a = z )
by A9, FUNCT_1:def 3;
consider b being
object such that A11:
(
b in dom (o . i) &
(o . i) . b = z )
by A9, FUNCT_1:def 3;
o _ (
x,
a)
= o _ (
i,
b)
by A10, A11;
hence
contradiction
by A10, A11, A5, A2, A1, Def6, A7;
verum
end; then A12:
rng ox c= D \ (rng (o . i))
by XBOOLE_1:86;
D \ (rng (o . i)) c= (rng F) \/ (D \ (rng (o . i)))
by XBOOLE_1:7;
then
rng ox c= (rng F) \/ (D \ (rng (o . i)))
by A12;
then
ox is
FinSequence of
(rng F) \/ (D \ (rng (o . i)))
by FINSEQ_1:def 4;
hence
y in ((rng F) \/ (D \ (rng (o . i)))) *
by A8, A5, FINSEQ_1:def 11;
verum end; end;
end;
then reconsider oF = o +* (i,F) as FinSequence of ((rng F) \/ (D \ (rng (o . i)))) * by FINSEQ_1:def 4;
A13:
oF is double-one-to-one
proof
let x1,
x2,
y1,
y2 be
object ;
FLEXARY1:def 6 ( x1 in dom oF & y1 in dom (oF . x1) & x2 in dom oF & y2 in dom (oF . x2) & oF _ (x1,y1) = oF _ (x2,y2) implies ( x1 = x2 & y1 = y2 ) )
assume A14:
(
x1 in dom oF &
y1 in dom (oF . x1) &
x2 in dom oF &
y2 in dom (oF . x2) &
oF _ (
x1,
y1)
= oF _ (
x2,
y2) )
;
( x1 = x2 & y1 = y2 )
per cases
( ( x1 = i & x2 = i ) or ( x1 = i & x2 <> i ) or ( x1 <> i & x2 = i ) or ( x1 <> i & x2 <> i ) )
;
suppose
(
x1 = i &
x2 = i )
;
( x1 = x2 & y1 = y2 )end; suppose A15:
(
x1 = i &
x2 <> i )
;
( x1 = x2 & y1 = y2 )then A16:
(oF . x1) . y1 in rng F
by A3, A14, FUNCT_1:def 3;
A17:
oF . x2 = o . x2
by A15, FUNCT_7:32;
then
(o . x2) . y2 in D
by A14, A2, Th1, A4;
then
(o . x2) . y2 in D /\ (rng F)
by A14, A17, A16, XBOOLE_0:def 4;
then consider y3 being
object such that A18:
(
y3 in dom (o . i) &
(o . i) . y3 = (o . x2) . y2 )
by A1, FUNCT_1:def 3;
o _ (
x2,
y2)
= o _ (
i,
y3)
by A18;
hence
(
x1 = x2 &
y1 = y2 )
by Def6, A2, A18, A14, A17, A15;
verum end; suppose A19:
(
x1 <> i &
x2 = i )
;
( x1 = x2 & y1 = y2 )then A20:
(oF . x2) . y2 in rng F
by A3, A14, FUNCT_1:def 3;
A21:
oF . x1 = o . x1
by A19, FUNCT_7:32;
then
(o . x1) . y1 in D
by A14, A2, Th1, A4;
then
(o . x1) . y1 in D /\ (rng F)
by A14, A21, A20, XBOOLE_0:def 4;
then consider y3 being
object such that A22:
(
y3 in dom (o . i) &
(o . i) . y3 = (o . x1) . y1 )
by A1, FUNCT_1:def 3;
o _ (
x1,
y1)
= o _ (
i,
y3)
by A22;
hence
(
x1 = x2 &
y1 = y2 )
by Def6, A2, A22, A14, A21, A19;
verum end; end;
end;
A24:
Values oF c= (rng F) \/ (D \ (rng (o . i)))
proof
let z be
object ;
TARSKI:def 3 ( not z in Values oF or z in (rng F) \/ (D \ (rng (o . i))) )
assume
z in Values oF
;
z in (rng F) \/ (D \ (rng (o . i)))
then consider x,
y being
object such that A25:
(
x in dom oF &
y in dom (oF . x) &
z = (oF . x) . y )
by Th1;
per cases
( x = i or x <> i )
;
suppose A26:
x <> i
;
z in (rng F) \/ (D \ (rng (o . i)))then A27:
oF . x = o . x
by FUNCT_7:32;
then A28:
z in D
by A4, A2, A25, Th1;
not
z in rng (o . i)
proof
assume
z in rng (o . i)
;
contradiction
then consider a being
object such that A29:
(
a in dom (o . i) &
(o . i) . a = z )
by FUNCT_1:def 3;
o _ (
i,
a)
= o _ (
x,
y)
by A26, FUNCT_7:32, A25, A29;
hence
contradiction
by A27, A25, A29, A1, A2, Def6, A26;
verum
end; then
z in D \ (rng (o . i))
by A28, XBOOLE_0:def 5;
hence
z in (rng F) \/ (D \ (rng (o . i)))
by XBOOLE_0:def 3;
verum end; end;
end;
A30:
D \ (rng (o . i)) c= Values oF
rng F c= Values oF
then
Values oF = (rng F) \/ (D \ (rng (o . i)))
by A30, XBOOLE_1:8, A24;
hence
o +* (i,F) is DoubleReorganization of (rng F) \/ (D \ (rng (o . i)))
by A13, Def7; verum