let n be Nat; :: thesis: for f being Element of REAL * holds OuterVx (f,n) c= UnusedVx (f,n)
let f be Element of REAL * ; :: thesis: OuterVx (f,n) c= UnusedVx (f,n)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in OuterVx (f,n) or x in UnusedVx (f,n) )
assume x in OuterVx (f,n) ; :: thesis: x in UnusedVx (f,n)
then ex k being Nat st
( x = k & k in dom f & 1 <= k & k <= n & f . k <> - 1 & f . (n + k) <> - 1 ) ;
hence x in UnusedVx (f,n) ; :: thesis: verum