let n be Element of 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 set ; :: 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 consider k being Element of NAT such that
A1: ( x = k & k in dom f & 1 <= k & k <= n & f . k <> - 1 & f . (n + k) <> - 1 ) ;
thus x in UnusedVx f,n by A1; :: thesis: verum