let X be set ; :: thesis: for F1, F2 being disjoint_valued FinSequence of X st union (rng F1) misses union (rng F2) holds
F1 ^ F2 is disjoint_valued FinSequence of X
let F1, F2 be disjoint_valued FinSequence of X; :: thesis: ( union (rng F1) misses union (rng F2) implies F1 ^ F2 is disjoint_valued FinSequence of X )
assume A1: union (rng F1) misses union (rng F2) ; :: thesis: F1 ^ F2 is disjoint_valued FinSequence of X
now :: thesis: for x, y being object st x <> y holds
(F1 ^ F2) . x misses (F1 ^ F2) . y
let x, y be object ; :: thesis: ( x <> y implies (F1 ^ F2) . b1 misses (F1 ^ F2) . b2 )
assume A2: x <> y ; :: thesis: (F1 ^ F2) . b1 misses (F1 ^ F2) . b2
per cases ( ( x in dom (F1 ^ F2) & y in dom (F1 ^ F2) ) or not x in dom (F1 ^ F2) or not y in dom (F1 ^ F2) ) ;
suppose A3: ( x in dom (F1 ^ F2) & y in dom (F1 ^ F2) ) ; :: thesis: (F1 ^ F2) . b1 misses (F1 ^ F2) . b2
then reconsider i = x, j = y as Nat ;
per cases ( i in dom F1 or not i in dom F1 ) ;
suppose A4: i in dom F1 ; :: thesis: (F1 ^ F2) . b1 misses (F1 ^ F2) . b2
then A5: (F1 ^ F2) . x = F1 . i by FINSEQ_1:def 7;
per cases ( j in dom F1 or not j in dom F1 ) ;
suppose j in dom F1 ; :: thesis: (F1 ^ F2) . b1 misses (F1 ^ F2) . b2
then (F1 ^ F2) . y = F1 . j by FINSEQ_1:def 7;
hence (F1 ^ F2) . x misses (F1 ^ F2) . y by A2, A5, PROB_2:def 2; :: thesis: verum
end;
suppose not j in dom F1 ; :: thesis: (F1 ^ F2) . b1 misses (F1 ^ F2) . b2
then consider j1 being Nat such that
A6: ( j1 in dom F2 & j = (len F1) + j1 ) by A3, FINSEQ_1:25;
(F1 ^ F2) . y = F2 . j1 by A6, FINSEQ_1:def 7;
then ( (F1 ^ F2) . x c= union (rng F1) & (F1 ^ F2) . y c= union (rng F2) ) by A4, A5, A6, FUNCT_1:3, ZFMISC_1:74;
hence (F1 ^ F2) . x misses (F1 ^ F2) . y by A1, XBOOLE_1:64; :: thesis: verum
end;
end;
end;
suppose not i in dom F1 ; :: thesis: (F1 ^ F2) . b1 misses (F1 ^ F2) . b2
then consider i1 being Nat such that
A7: ( i1 in dom F2 & i = (len F1) + i1 ) by A3, FINSEQ_1:25;
A8: (F1 ^ F2) . x = F2 . i1 by A7, FINSEQ_1:def 7;
per cases ( j in dom F1 or not j in dom F1 ) ;
suppose A9: j in dom F1 ; :: thesis: (F1 ^ F2) . b1 misses (F1 ^ F2) . b2
then (F1 ^ F2) . y = F1 . j by FINSEQ_1:def 7;
then ( (F1 ^ F2) . x c= union (rng F2) & (F1 ^ F2) . y c= union (rng F1) ) by A7, A8, A9, FUNCT_1:3, ZFMISC_1:74;
hence (F1 ^ F2) . x misses (F1 ^ F2) . y by A1, XBOOLE_1:64; :: thesis: verum
end;
suppose not j in dom F1 ; :: thesis: (F1 ^ F2) . b1 misses (F1 ^ F2) . b2
then consider j1 being Nat such that
A10: ( j1 in dom F2 & j = (len F1) + j1 ) by A3, FINSEQ_1:25;
(F1 ^ F2) . y = F2 . j1 by A10, FINSEQ_1:def 7;
hence (F1 ^ F2) . x misses (F1 ^ F2) . y by A2, A7, A10, A8, PROB_2:def 2; :: thesis: verum
end;
end;
end;
end;
end;
suppose ( not x in dom (F1 ^ F2) or not y in dom (F1 ^ F2) ) ; :: thesis: (F1 ^ F2) . b1 misses (F1 ^ F2) . b2
then ( (F1 ^ F2) . x = {} or (F1 ^ F2) . y = {} ) by FUNCT_1:def 2;
hence (F1 ^ F2) . x misses (F1 ^ F2) . y ; :: thesis: verum
end;
end;
end;
hence F1 ^ F2 is disjoint_valued FinSequence of X by PROB_2:def 2; :: thesis: verum