let i be Element of NAT ; :: thesis: for I being non empty FinSequence of NAT
for X being set st 1 <= i & i <= len I & rng I c= X holds
I /. i in X
let I be non empty FinSequence of NAT ; :: thesis: for X being set st 1 <= i & i <= len I & rng I c= X holds
I /. i in X
let X be set ; :: thesis: ( 1 <= i & i <= len I & rng I c= X implies I /. i in X )
assume AS: ( 1 <= i & i <= len I & rng I c= X ) ; :: thesis: I /. i in X
then i in Seg (len I) ;
then X1: i in dom I by FINSEQ_1:def 3;
then I . i in rng I by FUNCT_1:3;
then I /. i in rng I by X1, PARTFUN1:def 6;
hence I /. i in X by AS; :: thesis: verum