let f1, f2 be FinSequence of (TOP-REAL 2); :: thesis: ( f1 is one-to-one & f1 is special & 2 <= len f1 & f2 is one-to-one & f2 is special & 2 <= len f2 & X_axis f1 lies_between (X_axis f1) . 1,(X_axis f1) . (len f1) & X_axis f2 lies_between (X_axis f1) . 1,(X_axis f1) . (len f1) & Y_axis f1 lies_between (Y_axis f2) . 1,(Y_axis f2) . (len f2) & Y_axis f2 lies_between (Y_axis f2) . 1,(Y_axis f2) . (len f2) implies L~ f1 meets L~ f2 )
assume that
A1: ( f1 is one-to-one & f1 is special ) and
A2: 2 <= len f1 and
A3: ( f2 is one-to-one & f2 is special ) and
A4: ( 2 <= len f2 & X_axis f1 lies_between (X_axis f1) . 1,(X_axis f1) . (len f1) & X_axis f2 lies_between (X_axis f1) . 1,(X_axis f1) . (len f1) & Y_axis f1 lies_between (Y_axis f2) . 1,(Y_axis f2) . (len f2) & Y_axis f2 lies_between (Y_axis f2) . 1,(Y_axis f2) . (len f2) ) ; :: thesis: L~ f1 meets L~ f2
A5: for n being Nat st n in dom f2 & n + 1 in dom f2 holds
f2 /. n <> f2 /. (n + 1)
proof
let n be Nat; :: thesis: ( n in dom f2 & n + 1 in dom f2 implies f2 /. n <> f2 /. (n + 1) )
assume ( n in dom f2 & n + 1 in dom f2 & f2 /. n = f2 /. (n + 1) ) ; :: thesis: contradiction
then n = n + 1 by A3, PARTFUN2:10;
hence contradiction ; :: thesis: verum
end;
for n being Nat st n in dom f1 & n + 1 in dom f1 holds
f1 /. n <> f1 /. (n + 1)
proof
let n be Nat; :: thesis: ( n in dom f1 & n + 1 in dom f1 implies f1 /. n <> f1 /. (n + 1) )
assume ( n in dom f1 & n + 1 in dom f1 & f1 /. n = f1 /. (n + 1) ) ; :: thesis: contradiction
then n = n + 1 by A1, PARTFUN2:10;
hence contradiction ; :: thesis: verum
end;
hence L~ f1 meets L~ f2 by A1, A2, A3, A4, A5, Th4; :: thesis: verum