let f1, f2 be disjoint_valued FinSequence; :: thesis: ex f being disjoint_valued FinSequence st
( (Union f1) /\ (Union f2) = Union f & dom f = Seg ((len f1) * (len f2)) & ( for i being Nat st i in dom f holds
f . i = (f1 . (((i -' 1) div (len f2)) + 1)) /\ (f2 . (((i -' 1) mod (len f2)) + 1)) ) )
consider f being FinSequence such that
A1: ( (Union f1) /\ (Union f2) = Union f & dom f = Seg ((len f1) * (len f2)) & ( for i being Nat st i in dom f holds
f . i = (f1 . (((i -' 1) div (len f2)) + 1)) /\ (f2 . (((i -' 1) mod (len f2)) + 1)) ) ) by TT1;
now :: thesis: for i, j being object st i <> j holds
f . i misses f . j
let i, j be object ; :: thesis: ( i <> j implies f . b1 misses f . b2 )
assume A2: i <> j ; :: thesis: f . b1 misses f . b2
per cases ( ( i in dom f & j in dom f ) or not i in dom f or not j in dom f ) ;
suppose A3: ( i in dom f & j in dom f ) ; :: thesis: f . b1 misses f . b2
then reconsider i1 = i, j1 = j as Nat ;
( f . i = (f1 . (((i1 -' 1) div (len f2)) + 1)) /\ (f2 . (((i1 -' 1) mod (len f2)) + 1)) & f . j = (f1 . (((j1 -' 1) div (len f2)) + 1)) /\ (f2 . (((j1 -' 1) mod (len f2)) + 1)) ) by A1, A3;
then B1: ( f . i c= f1 . (((i1 -' 1) div (len f2)) + 1) & f . j c= f1 . (((j1 -' 1) div (len f2)) + 1) & f . i c= f2 . (((i1 -' 1) mod (len f2)) + 1) & f . j c= f2 . (((j1 -' 1) mod (len f2)) + 1) ) by XBOOLE_1:17;
A5: ( ( 0 < len f1 & 0 < len f2 ) or ( 0 > len f1 & 0 > len f2 ) ) by A1, A3;
A6: now :: thesis: ( ((i1 -' 1) div (len f2)) + 1 = ((j1 -' 1) div (len f2)) + 1 implies not ((i1 -' 1) mod (len f2)) + 1 = ((j1 -' 1) mod (len f2)) + 1 )
assume A7: ( ((i1 -' 1) div (len f2)) + 1 = ((j1 -' 1) div (len f2)) + 1 & ((i1 -' 1) mod (len f2)) + 1 = ((j1 -' 1) mod (len f2)) + 1 ) ; :: thesis: contradiction
i1 -' 1 = ((len f2) * ((j1 -' 1) div (len f2))) + ((i1 -' 1) mod (len f2)) by A7, A5, NAT_D:2
.= j1 -' 1 by A5, A7, NAT_D:2 ;
then ( ( 1 > i1 or i1 >= j1 ) & ( 1 > j1 or j1 >= i1 ) ) by NAT_D:56;
hence contradiction by A2, A1, A3, FINSEQ_1:1, XXREAL_0:1; :: thesis: verum
end;
per cases ( ((i1 -' 1) div (len f2)) + 1 <> ((j1 -' 1) div (len f2)) + 1 or ((i1 -' 1) mod (len f2)) + 1 <> ((j1 -' 1) mod (len f2)) + 1 ) by A6;
suppose ((i1 -' 1) div (len f2)) + 1 <> ((j1 -' 1) div (len f2)) + 1 ; :: thesis: f . b1 misses f . b2
hence f . i misses f . j by B1, XBOOLE_1:64, PROB_2:def 2; :: thesis: verum
end;
suppose ((i1 -' 1) mod (len f2)) + 1 <> ((j1 -' 1) mod (len f2)) + 1 ; :: thesis: f . b1 misses f . b2
hence f . i misses f . j by B1, XBOOLE_1:64, PROB_2:def 2; :: thesis: verum
end;
end;
end;
suppose ( not i in dom f or not j in dom f ) ; :: thesis: f . b1 misses f . b2
then ( f . i = {} or f . j = {} ) by FUNCT_1:def 2;
hence f . i misses f . j ; :: thesis: verum
end;
end;
end;
then reconsider f = f as disjoint_valued FinSequence by PROB_2:def 2;
take f ; :: thesis: ( (Union f1) /\ (Union f2) = Union f & dom f = Seg ((len f1) * (len f2)) & ( for i being Nat st i in dom f holds
f . i = (f1 . (((i -' 1) div (len f2)) + 1)) /\ (f2 . (((i -' 1) mod (len f2)) + 1)) ) )
thus ( (Union f1) /\ (Union f2) = Union f & dom f = Seg ((len f1) * (len f2)) & ( for i being Nat st i in dom f holds
f . i = (f1 . (((i -' 1) div (len f2)) + 1)) /\ (f2 . (((i -' 1) mod (len f2)) + 1)) ) ) by A1; :: thesis: verum