let it1, it2 be Element of NAT ; :: thesis: ( OuterVx ((((repeat f) . it1) . g),n) = {} & ( for k being Nat st OuterVx ((((repeat f) . k) . g),n) = {} holds
it1 <= k ) & OuterVx ((((repeat f) . it2) . g),n) = {} & ( for k being Nat st OuterVx ((((repeat f) . k) . g),n) = {} holds
it2 <= k ) implies it1 = it2 )
assume A4: ( OuterVx ((((repeat f) . it1) . g),n) = {} & ( for k being Nat st OuterVx ((((repeat f) . k) . g),n) = {} holds
it1 <= k ) & OuterVx ((((repeat f) . it2) . g),n) = {} & ( for k being Nat st OuterVx ((((repeat f) . k) . g),n) = {} holds
it2 <= k ) & not it1 = it2 ) ; :: thesis: contradiction
then ( it1 <= it2 & it2 <= it1 ) ;
hence contradiction by A4, XXREAL_0:1; :: thesis: verum