let n be Element of NAT ; :: thesis: for c being set st 1 <= n holds
rng (IdFinS c,n) = rng <*c*>
let c be set ; :: thesis: ( 1 <= n implies rng (IdFinS c,n) = rng <*c*> )
assume A1: 1 <= n ; :: thesis: rng (IdFinS c,n) = rng <*c*>
n in Seg n by A1, FINSEQ_1:3;
then A2: (IdFinS c,n) . n = c by FUNCOP_1:13;
thus rng (IdFinS c,n) c= rng <*c*> :: according to XBOOLE_0:def 10 :: thesis: rng <*c*> c= rng (IdFinS c,n)

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in rng (IdFinS c,n) or a in rng <*c*> )
assume a in rng (IdFinS c,n) ; :: thesis: a in rng <*c*>
then consider i being Nat such that
A3: i in dom (IdFinS c,n) and
A4: (IdFinS c,n) . i = a by FINSEQ_2:11;
i in Seg (len (IdFinS c,n)) by A3, FINSEQ_1:def 3;
then i in Seg n by FINSEQ_1:def 18;
then a = c by A4, FUNCOP_1:13;
then a in {c} by TARSKI:def 1;
hence a in rng <*c*> by FINSEQ_1:55; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in rng <*c*> or a in rng (IdFinS c,n) )
assume a in rng <*c*> ; :: thesis: a in rng (IdFinS c,n)
then a in {c} by FINSEQ_1:55;
then A5: a = c by TARSKI:def 1;
n = len (IdFinS c,n) by FINSEQ_1:def 18;
then n in dom (IdFinS c,n) by A1, FINSEQ_3:27;
hence a in rng (IdFinS c,n) by A5, A2, FUNCT_1:def 5; :: thesis: verum