let I, J be FinSequence-membered set ; :: thesis: for p, q being FinSequence st len p = len q & p <> q holds
p ^^ I misses q ^^ J
let p, q be FinSequence; :: thesis: ( len p = len q & p <> q implies p ^^ I misses q ^^ J )
assume Z0: len p = len q ; :: thesis: ( not p <> q or p ^^ I misses q ^^ J )
assume Z1: p <> q ; :: thesis: p ^^ I misses q ^^ J
assume p ^^ I meets q ^^ J ; :: thesis: contradiction
then consider a being object such that
A1: ( a in p ^^ I & a in q ^^ J ) by XBOOLE_0:3;
consider p1 being Element of I such that
A2: ( a = p ^ p1 & p1 in I ) by A1;
consider q1 being Element of J such that
A3: ( a = q ^ q1 & q1 in J ) by A1;
( dom p = Seg (len p) & dom q = Seg (len q) ) by FINSEQ_1:def 3;
then ( p = (p ^ p1) | (dom p) & (p ^ p1) | (dom p) = q ) by A2, A3, Z0, FINSEQ_1:21;
hence contradiction by Z1; :: thesis: verum