let i be Nat; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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) ) ; :: thesis: 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 ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (o +* (i,F)) or y in ((rng F) \/ (D \ (rng (o . i)))) * )
assume y in rng (o +* (i,F)) ; :: thesis: 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 x = i ; :: thesis: y in ((rng F) \/ (D \ (rng (o . i)))) *

then A6: y = F by A5, A1, FUNCT_7:31;
F is FinSequence of (rng F) \/ (D \ (rng (o . i))) by XBOOLE_1:7, FINSEQ_1:def 4;
hence y in ((rng F) \/ (D \ (rng (o . i)))) * by A6, FINSEQ_1:def 11; :: thesis: verum

end;

suppose A7: x <> i ; :: thesis: 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) ; :: thesis: 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; :: thesis: 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; :: thesis: 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 ; :: according to FLEXARY1:def 6 :: thesis: ( 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) ) ; :: thesis: ( 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 ) ; :: thesis: ( x1 = x2 & y1 = y2 )

hence ( x1 = x2 & y1 = y2 ) by A3, A14, FUNCT_1:def 4; :: thesis: verum

end;

suppose A15: ( x1 = i & x2 <> i ) ; :: thesis: ( 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; :: thesis: verum

end;

suppose A19: ( x1 <> i & x2 = i ) ; :: thesis: ( 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; :: thesis: verum

end;

suppose ( x1 <> i & x2 <> i ) ; :: thesis: ( x1 = x2 & y1 = y2 )

then A23: ( o . x1 = oF . x1 & o . x2 = oF . x2 ) by FUNCT_7:32;
then o _ (x1,y1) = o _ (x2,y2) by A14;
hence ( x1 = x2 & y1 = y2 ) by A23, A14, A2, Def6; :: thesis: verum

end;

end;

end;

A24: Values oF c= (rng F) \/ (D \ (rng (o . i)))

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Values oF or z in (rng F) \/ (D \ (rng (o . i))) )
assume z in Values oF ; :: thesis: 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 x = i ; :: thesis: z in (rng F) \/ (D \ (rng (o . i)))

then oF . x = F by A1, FUNCT_7:31;
then z in rng F by A25, FUNCT_1:def 3;
hence z in (rng F) \/ (D \ (rng (o . i))) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose A26: x <> i ; :: thesis: 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) ; :: thesis: 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; :: thesis: 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; :: thesis: verum

end;

end;

end;

A30: D \ (rng (o . i)) c= Values oF

proof

let d be object ; :: according to TARSKI:def 3 :: thesis: ( not d in D \ (rng (o . i)) or d in Values oF )
assume A31: d in D \ (rng (o . i)) ; :: thesis: d in Values oF
then A32: ( d in D & not d in rng (o . i) ) by XBOOLE_0:def 5;
consider x, y being object such that
A33: ( x in dom o & y in dom (o . x) & d = (o . x) . y ) by A31, Th1, A4;
x <> i by A33, FUNCT_1:def 3, A32;
then o . x = oF . x by FUNCT_7:32;
hence d in Values oF by Th1, A2, A33; :: thesis: verum

end;

rng F c= Values oF

proof

let d be object ; :: according to TARSKI:def 3 :: thesis: ( not d in rng F or d in Values oF )
assume d in rng F ; :: thesis: d in Values oF
then ex x being object st
( x in dom F & F . x = d ) by FUNCT_1:def 3;
hence d in Values oF by A1, A2, A3, Th1; :: thesis: verum

end;

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; :: thesis: verum