let f, g be FinSequence of (TOP-REAL 2); ( g is_Shortcut_of f implies L~ g c= L~ f )
assume A1:
g is_Shortcut_of f
; L~ g c= L~ f
let x be object ; TARSKI:def 3 ( not x in L~ g or x in L~ f )
assume
x in L~ g
; x in L~ f
then
x in union { (LSeg (g,i)) where i is Nat : ( 1 <= i & i + 1 <= len g ) }
by TOPREAL1:def 4;
then consider y being set such that
A2:
( x in y & y in { (LSeg (g,i)) where i is Nat : ( 1 <= i & i + 1 <= len g ) } )
by TARSKI:def 4;
consider i being Nat such that
A3:
y = LSeg (g,i)
and
A4:
( 1 <= i & i + 1 <= len g )
by A2;
consider k1 being Element of NAT such that
A5:
( 1 <= k1 & k1 + 1 <= len f )
and
A6:
( f /. k1 = g /. i & f /. (k1 + 1) = g /. (i + 1) )
and
f . k1 = g . i
and
f . (k1 + 1) = g . (i + 1)
by A1, A4, Th21;
A7:
LSeg (f,k1) in { (LSeg (f,k)) where k is Nat : ( 1 <= k & k + 1 <= len f ) }
by A5;
x in LSeg ((g /. i),(g /. (i + 1)))
by A2, A3, A4, TOPREAL1:def 3;
then
x in LSeg (f,k1)
by A5, A6, TOPREAL1:def 3;
then
x in union { (LSeg (f,k)) where k is Nat : ( 1 <= k & k + 1 <= len f ) }
by A7, TARSKI:def 4;
hence
x in L~ f
by TOPREAL1:def 4; verum