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 A1: ( 1 <= i & i <= len I & rng I c= X ) ; :: thesis: I /. i in X
then A2: i in dom I by FINSEQ_3:25;
then I . i in rng I by FUNCT_1:3;
then I /. i in rng I by A2, PARTFUN1:def 6;
hence I /. i in X by A1; :: thesis: verum