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;

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 )
;

end;

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;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

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

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

end;now :: thesis: ( ( 1 < i & x in rng f ) or ( 1 >= i & x in rng f ) )end;

hence
x in rng f
; :: thesis: verumper cases
( 1 < i or 1 >= i )
;

end;

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;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