let f, g be FinSequence of (TOP-REAL 2); :: thesis: ( g is_Shortcut_of f implies rng g c= rng f )
assume A1: g is_Shortcut_of f ; :: thesis: rng g c= rng f
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng g or x in rng f )
assume x in rng g ; :: thesis: x in rng f
then consider z being set such that
A2: ( z in dom g & x = g . z ) by FUNCT_1:def 5;
A3: z in Seg (len g) by A2, FINSEQ_1:def 3;
reconsider i = z as Element of NAT by A2;
A4: ( 1 <= i & i <= len g ) by A3, FINSEQ_1:3;

per cases ( i < len g or i >= len g ) ;

suppose i < len g ; :: thesis: x in rng f

then i + 1 <= len g by NAT_1:13;
then 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, A4, Th25;
k1 < len f by A5, NAT_1:13;
then k1 in dom f by A5, FINSEQ_3:27;
hence x in rng f by A2, A5, FUNCT_1:def 5; :: thesis: verum

end;

suppose i >= len g ; :: thesis: x in rng f

then A6: i = len g by A4, XXREAL_0:1;

now

per cases ( 1 < i or 1 >= i ) ;

case A7: 1 < i ; :: thesis: x in rng f

then 1 - 1 < i - 1 by XREAL_1:11;
then 0 < i -' 1 by A7, XREAL_1:235;
then A8: 0 + 1 <= i -' 1 by NAT_1:13;
A9: i -' 1 = i - 1 by A7, XREAL_1:235;
then consider k1 being Element of NAT such that
A10: ( 1 <= k1 & k1 + 1 <= len f & f /. k1 = g /. (i -' 1) & f /. (k1 + 1) = g /. ((i -' 1) + 1) & f . k1 = g . (i -' 1) & f . (k1 + 1) = g . ((i -' 1) + 1) ) by A1, A4, A8, Th25;
1 < k1 + 1 by A10, NAT_1:13;
then k1 + 1 in dom f by A10, FINSEQ_3:27;
hence x in rng f by A2, A9, A10, FUNCT_1:def 5; :: thesis: verum

end;

case 1 >= i ; :: thesis: x in rng f

then A11: i = 1 by A4, XXREAL_0:1;
A12: f . 1 = g . 1 by A1, Def3;
len g <= len f by A1, Th12;
then 1 in dom f by A6, A11, FINSEQ_3:27;
hence x in rng f by A2, A11, A12, FUNCT_1:def 5; :: thesis: verum

end;

end;

end;

hence x in rng f ; :: thesis: verum

end;

end;