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

proof

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

end;

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

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (l . i) where i is Nat : ( 1 <= i & i <= len l ) } or a in rng l )
assume a in { (l . i) where i is Nat : ( 1 <= i & i <= len l ) } ; :: thesis: a in rng l
then consider k being Nat such that
A4: a = l . k and
A5: 1 <= k and
A6: k <= len l ;
k in dom l by A5, A6, FINSEQ_3:25;
hence a in rng l by A4, FUNCT_1:def 3; :: thesis: verum

end;