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*>
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 A2: a in rng (IdFinS c,n) ; :: thesis: a in rng <*c*>
consider i being Nat such that
A3: ( i in dom (IdFinS c,n) & (IdFinS c,n) . i = a ) by A2, 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 A3, 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 A4: a in rng <*c*> ; :: thesis: a in rng (IdFinS c,n)
a in {c} by A4, FINSEQ_1:55;
then A5: a = c by TARSKI:def 1;
n = len (IdFinS c,n) by FINSEQ_1:def 18;
then A6: n in dom (IdFinS c,n) by A1, FINSEQ_3:27;
n in Seg n by A1, FINSEQ_1:3;
then (IdFinS c,n) . n = c by FUNCOP_1:13;
hence a in rng (IdFinS c,n) by A5, A6, FUNCT_1:def 5; :: thesis: verum