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:1;
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: 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:10;
i in Seg (len (IdFinS (c,n))) by A3, FINSEQ_1:def 3;
then i in Seg n by CARD_1:def 7;
then a = c by A4, FUNCOP_1:7;
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 A1, FINSEQ_3:25;
hence a in rng (IdFinS (c,n)) by A5, A2, FUNCT_1:def 3; :: thesis: verum