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 ;
then A2: (IdFinS (c,n)) . n = c by FUNCOP_1:7;
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 object ; :: 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:
then consider i being Nat such that
A3: i in dom (IdFinS (c,n)) and
A4: (IdFinS (c,n)) . i = a by FINSEQ_2:10;
i in Seg (len (IdFinS (c,n))) by ;
then i in Seg n by CARD_1:def 7;
then a = c by ;
then a in {c} by TARSKI:def 1;
hence a in rng <*c*> by FINSEQ_1:38; :: thesis: verum
end;
let a be object ; :: 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:38;
then A5: a = c by TARSKI:def 1;
n = len (IdFinS (c,n)) by CARD_1:def 7;
then n in dom (IdFinS (c,n)) by ;
hence a in rng (IdFinS (c,n)) by ; :: thesis: verum