let n be Element of NAT ; :: thesis: for f being Element of REAL * holds UnusedVx f,n c= Seg n
let f be Element of REAL * ; :: thesis: UnusedVx f,n c= Seg n
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in UnusedVx f,n or x in Seg n )
assume x in UnusedVx f,n ; :: thesis: x in Seg n
then consider i being Element of NAT such that
A1: ( x = i & i in dom f & 1 <= i & i <= n & f . i <> - 1 ) ;
x in { k where k is Element of NAT : ( 1 <= k & k <= n ) } by A1;
hence x in Seg n by FINSEQ_1:def 1; :: thesis: verum