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 object ; :: 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 object such that
A2: z in dom g and
A3: x = g . z by FUNCT_1:def 3;
reconsider i = z as Element of NAT by A2;
A4: z in Seg (len g) by A2, FINSEQ_1:def 3;
then A5: 1 <= i by FINSEQ_1:1;
A6: i <= len g by A4, FINSEQ_1:1;
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
A7: 1 <= k1 and
A8: k1 + 1 <= len f and
f /. k1 = g /. i and
f /. (k1 + 1) = g /. (i + 1) and
A9: f . k1 = g . i and
f . (k1 + 1) = g . (i + 1) by A1, A5, Th21;
k1 < len f by A8, NAT_1:13;
then k1 in dom f by A7, FINSEQ_3:25;
hence x in rng f by A3, A9, FUNCT_1:def 3; :: thesis: verum
end;
suppose i >= len g ; :: thesis: x in rng f
then A10: i = len g by A6, XXREAL_0:1;
now :: thesis: ( ( 1 < i & x in rng f ) or ( 1 >= i & x in rng f ) )
per cases ( 1 < i or 1 >= i ) ;
case A11: 1 < i ; :: thesis: x in rng f
then A12: i -' 1 = i - 1 by XREAL_1:233;
1 - 1 < i - 1 by A11, XREAL_1:9;
then 0 < i -' 1 by A11, XREAL_1:233;
then 0 + 1 <= i -' 1 by NAT_1:13;
then consider k1 being Element of NAT such that
A13: 1 <= k1 and
A14: k1 + 1 <= len f and
f /. k1 = g /. (i -' 1) and
f /. (k1 + 1) = g /. ((i -' 1) + 1) and
f . k1 = g . (i -' 1) and
A15: f . (k1 + 1) = g . ((i -' 1) + 1) by A1, A6, A12, Th21;
1 < k1 + 1 by A13, NAT_1:13;
then k1 + 1 in dom f by A14, FINSEQ_3:25;
hence x in rng f by A3, A12, A15, FUNCT_1:def 3; :: thesis: verum
end;
end;
end;
hence x in rng f ; :: thesis: verum
end;
end;