let f1, f2 be FinSequence; :: thesis: ( f1 is disjoint_valued & f2 is disjoint_valued & union (rng f1) misses union (rng f2) implies f1 ^ f2 is disjoint_valued )
assume that
A1: ( f1 is disjoint_valued & f2 is disjoint_valued ) and
A2: union (rng f1) misses union (rng f2) ; :: thesis: f1 ^ f2 is disjoint_valued

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) . b₁ misses (f1 ^ f2) . b₂ )
assume A3: x <> y ; :: thesis: (f1 ^ f2) . b₁ misses (f1 ^ f2) . b₂

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 A4: ( x in dom (f1 ^ f2) & y in dom (f1 ^ f2) ) ; :: thesis: (f1 ^ f2) . b₁ misses (f1 ^ f2) . b₂

then reconsider x1 = x, y1 = y as Nat ;

per cases ( ( x1 in dom f1 & y1 in dom f1 ) or ( x1 in dom f1 & ex n being Nat st
( n in dom f2 & y1 = (len f1) + n ) ) or ( y1 in dom f1 & ex n being Nat st
( n in dom f2 & x1 = (len f1) + n ) ) or ( ex n being Nat st
( n in dom f2 & x1 = (len f1) + n ) & ex m being Nat st
( m in dom f2 & y1 = (len f1) + m ) ) ) by A4, FINSEQ_1:25;

suppose ( x1 in dom f1 & y1 in dom f1 ) ; :: thesis: (f1 ^ f2) . b₁ misses (f1 ^ f2) . b₂

then ( (f1 ^ f2) . x = f1 . x & (f1 ^ f2) . y = f1 . y ) by FINSEQ_1:def 7;
hence (f1 ^ f2) . x misses (f1 ^ f2) . y by A1, A3, PROB_2:def 2; :: thesis: verum

end;

suppose A6: ( x1 in dom f1 & ex n being Nat st
( n in dom f2 & y1 = (len f1) + n ) ) ; :: thesis: (f1 ^ f2) . b₁ misses (f1 ^ f2) . b₂

then consider n being Nat such that
A7: ( n in dom f2 & y1 = (len f1) + n ) ;
(f1 ^ f2) . x = f1 . x by A6, FINSEQ_1:def 7;
then A8: (f1 ^ f2) . x in rng f1 by A6, FUNCT_1:3;
(f1 ^ f2) . y = f2 . n by A7, FINSEQ_1:def 7;
then A9: (f1 ^ f2) . y in rng f2 by A7, FUNCT_1:3;

now :: thesis: not (f1 ^ f2) . x meets (f1 ^ f2) . y

assume (f1 ^ f2) . x meets (f1 ^ f2) . y ; :: thesis: contradiction
then consider z being object such that
A10: ( z in (f1 ^ f2) . x & z in (f1 ^ f2) . y ) by XBOOLE_0:3;
( z in union (rng f1) & z in union (rng f2) ) by A8, A9, A10, TARSKI:def 4;
hence contradiction by A2, XBOOLE_0:3; :: thesis: verum

end;

hence (f1 ^ f2) . x misses (f1 ^ f2) . y ; :: thesis: verum

end;

suppose A11: ( y1 in dom f1 & ex n being Nat st
( n in dom f2 & x1 = (len f1) + n ) ) ; :: thesis: (f1 ^ f2) . b₁ misses (f1 ^ f2) . b₂

then consider n being Nat such that
A12: ( n in dom f2 & x1 = (len f1) + n ) ;
(f1 ^ f2) . x = f2 . n by A12, FINSEQ_1:def 7;
then A13: (f1 ^ f2) . x in rng f2 by A12, FUNCT_1:3;
(f1 ^ f2) . y = f1 . y by A11, FINSEQ_1:def 7;
then A14: (f1 ^ f2) . y in rng f1 by A11, FUNCT_1:3;

now :: thesis: not (f1 ^ f2) . x meets (f1 ^ f2) . y

assume (f1 ^ f2) . x meets (f1 ^ f2) . y ; :: thesis: contradiction
then consider z being object such that
A15: ( z in (f1 ^ f2) . x & z in (f1 ^ f2) . y ) by XBOOLE_0:3;
( z in union (rng f1) & z in union (rng f2) ) by A13, A14, A15, TARSKI:def 4;
hence contradiction by A2, XBOOLE_0:3; :: thesis: verum

end;

hence (f1 ^ f2) . x misses (f1 ^ f2) . y ; :: thesis: verum

end;

suppose A16: ( ex n being Nat st
( n in dom f2 & x1 = (len f1) + n ) & ex m being Nat st
( m in dom f2 & y1 = (len f1) + m ) ) ; :: thesis: (f1 ^ f2) . b₁ misses (f1 ^ f2) . b₂

then consider n being Nat such that
A17: ( n in dom f2 & x1 = (len f1) + n ) ;
A18: (f1 ^ f2) . x = f2 . n by A17, FINSEQ_1:def 7;
consider m being Nat such that
A19: ( m in dom f2 & y1 = (len f1) + m ) by A16;
(f1 ^ f2) . y = f2 . m by A19, FINSEQ_1:def 7;
hence (f1 ^ f2) . x misses (f1 ^ f2) . y by A1, A18, A17, A19, A3, PROB_2:def 2; :: thesis: verum

end;

end;

end;

suppose ( not x in dom (f1 ^ f2) or not y in dom (f1 ^ f2) ) ; :: thesis: (f1 ^ f2) . b₁ misses (f1 ^ f2) . b₂

then ( (f1 ^ f2) . x = {} or (f1 ^ f2) . y = {} ) by FUNCT_1:def 2;
hence (f1 ^ f2) . x misses (f1 ^ f2) . y by XBOOLE_1:65; :: thesis: verum

end;

end;

end;

hence f1 ^ f2 is disjoint_valued by PROB_2:def 2; :: thesis: verum