let l be FinSequence; :: thesis: rng l = { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l ) }
thus rng l c= { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l ) } :: according to XBOOLE_0:def 10 :: thesis: { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l ) } c= rng l

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in rng l or a in { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l ) } )
assume a in rng l ; :: thesis: a in { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l ) }
then consider x being set such that
A1: ( x in dom l & a = l . x ) by FUNCT_1:def 5;
reconsider k = x as Element of NAT by A1;
( 1 <= k & k <= len l ) by A1, FINSEQ_3:27;
hence a in { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l ) } by A1; :: thesis: verum

end;

thus { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l ) } c= rng l :: thesis: verum

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l ) } or a in rng l )
assume a in { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l ) } ; :: thesis: a in rng l
then consider k being Element of NAT such that
A2: ( a = l . k & 1 <= k & k <= len l ) ;
k in dom l by A2, FINSEQ_3:27;
hence a in rng l by A2, FUNCT_1:def 5; :: thesis: verum

end;