let n be 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 object ; :: 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 ex i being Nat st

( x = i & i in dom f & 1 <= i & i <= n & f . i <> - 1 ) ;

then x in { k where k is Nat : ( 1 <= k & k <= n ) } ;

hence x in Seg n by FINSEQ_1:def 1; :: thesis: verum

let f be Element of REAL * ; :: thesis: UnusedVx (f,n) c= Seg n

let x be object ; :: 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 ex i being Nat st

( x = i & i in dom f & 1 <= i & i <= n & f . i <> - 1 ) ;

then x in { k where k is Nat : ( 1 <= k & k <= n ) } ;

hence x in Seg n by FINSEQ_1:def 1; :: thesis: verum