let f, g be FinSequence of (); :: 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 ;
then A5: 1 <= i by FINSEQ_1:1;
A6: i <= len g by ;
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 ;
then k1 in dom f by ;
hence x in rng f by ; :: thesis: verum
end;
suppose i >= len g ; :: thesis: x in rng f
then A10: i = len g by ;
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 ;
then 0 < i -' 1 by ;
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 ;
then k1 + 1 in dom f by ;
hence x in rng f by ; :: thesis: verum
end;
case 1 >= i ; :: thesis: x in rng f
then A16: i = 1 by ;
A17: f . 1 = g . 1 by A1;
len g <= len f by ;
then 1 in dom f by ;
hence x in rng f by ; :: thesis: verum
end;
end;
end;
hence x in rng f ; :: thesis: verum
end;
end;