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