let X be non empty set ; :: thesis: for S being SigmaField of X
for E1, E2 being Element of S st E1 misses E2 holds
<*E1,E2*> is Finite_Sep_Sequence of S
let S be SigmaField of X; :: thesis: for E1, E2 being Element of S st E1 misses E2 holds
<*E1,E2*> is Finite_Sep_Sequence of S
let E1, E2 be Element of S; :: thesis: ( E1 misses E2 implies <*E1,E2*> is Finite_Sep_Sequence of S )
assume A0: E1 misses E2 ; :: thesis: <*E1,E2*> is Finite_Sep_Sequence of S
A2: dom <*E1,E2*> = {1,2} by FINSEQ_1:92;
now :: thesis: for m, n being object st m <> n holds
<*E1,E2*> . m misses <*E1,E2*> . n
let m, n be object ; :: thesis: ( m <> n implies <*E1,E2*> . b1 misses <*E1,E2*> . b2 )
assume A3: m <> n ; :: thesis: <*E1,E2*> . b1 misses <*E1,E2*> . b2
per cases ( ( m in dom <*E1,E2*> & n in dom <*E1,E2*> ) or not m in dom <*E1,E2*> or not n in dom <*E1,E2*> ) ;
suppose ( m in dom <*E1,E2*> & n in dom <*E1,E2*> ) ; :: thesis: <*E1,E2*> . b1 misses <*E1,E2*> . b2
then ( ( m = 1 or m = 2 ) & ( n = 1 or n = 2 ) ) by A2, TARSKI:def 2;
then ( ( <*E1,E2*> . m = E1 & <*E1,E2*> . n = E2 ) or ( <*E1,E2*> . m = E2 & <*E1,E2*> . n = E1 ) ) by A3, FINSEQ_1:44;
hence <*E1,E2*> . m misses <*E1,E2*> . n by A0; :: thesis: verum
end;
suppose ( not m in dom <*E1,E2*> or not n in dom <*E1,E2*> ) ; :: thesis: <*E1,E2*> . b1 misses <*E1,E2*> . b2
then ( <*E1,E2*> . m = {} or <*E1,E2*> . n = {} ) by FUNCT_1:def 2;
hence <*E1,E2*> . m misses <*E1,E2*> . n ; :: thesis: verum
end;
end;
end;
then <*E1,E2*> is disjoint_valued ;
hence <*E1,E2*> is Finite_Sep_Sequence of S ; :: thesis: verum