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))

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

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 <*c*> or a in rng (IdFinS (c,n)) )
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;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

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