let D1, D2 be finite set ; :: thesis: ( D1 misses D2 implies for o1 being DoubleReorganization of D1
for o2 being DoubleReorganization of D2 holds o1 ^ o2 is DoubleReorganization of D1 \/ D2 )
assume A1: D1 misses D2 ; :: thesis: for o1 being DoubleReorganization of D1
for o2 being DoubleReorganization of D2 holds o1 ^ o2 is DoubleReorganization of D1 \/ D2
let o1 be DoubleReorganization of D1; :: thesis: for o2 being DoubleReorganization of D2 holds o1 ^ o2 is DoubleReorganization of D1 \/ D2
let o2 be DoubleReorganization of D2; :: thesis: o1 ^ o2 is DoubleReorganization of D1 \/ D2
set D = D1 \/ D2;
rng o1 c= (D1 \/ D2) *

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng o1 or x in (D1 \/ D2) * )
assume x in rng o1 ; :: thesis: x in (D1 \/ D2) *
then reconsider x = x as FinSequence of D1 by FINSEQ_1:def 11;
( rng x c= D1 & D1 c= D1 \/ D2 ) by XBOOLE_1:7;
then rng x c= D1 \/ D2 ;
then x is FinSequence of D1 \/ D2 by FINSEQ_1:def 4;
hence x in (D1 \/ D2) * by FINSEQ_1:def 11; :: thesis: verum

end;

then reconsider O1 = o1 as FinSequence of (D1 \/ D2) * by FINSEQ_1:def 4;
rng o2 c= (D1 \/ D2) *

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng o2 or x in (D1 \/ D2) * )
assume x in rng o2 ; :: thesis: x in (D1 \/ D2) *
then reconsider x = x as FinSequence of D2 by FINSEQ_1:def 11;
( rng x c= D2 & D2 c= D1 \/ D2 ) by XBOOLE_1:7;
then rng x c= D1 \/ D2 ;
then x is FinSequence of D1 \/ D2 by FINSEQ_1:def 4;
hence x in (D1 \/ D2) * by FINSEQ_1:def 11; :: thesis: verum

end;

then reconsider O2 = o2 as FinSequence of (D1 \/ D2) * by FINSEQ_1:def 4;
A2: ( Values o1 = D1 & Values o2 = D2 ) by Def7;
then A3: O1 ^ O2 is double-one-to-one by A1, Th33;
Values (O1 ^ O2) = D1 \/ D2 by A2, Th2;
hence o1 ^ o2 is DoubleReorganization of D1 \/ D2 by A3, Def7; :: thesis: verum