let n be non empty Nat; :: thesis: for f being NtoSEG Function of n,(Seg n)
for i being Nat st i < n holds
( f . i = i + 1 & i in dom f )
let f be NtoSEG Function of n,(Seg n); :: thesis: for i being Nat st i < n holds
( f . i = i + 1 & i in dom f )
let i be Nat; :: thesis: ( i < n implies ( f . i = i + 1 & i in dom f ) )
assume i < n ; :: thesis: ( f . i = i + 1 & i in dom f )
then L0: i in n by NAT_1:44;
then consider ii being Element of n such that
L1: ii = i ;
L2: ntoSeg ii = ii + 1 ;
thus f . i = i + 1 by defNtoSEG, L1, L2; :: thesis: i in dom f
thus i in dom f by L0, FUNCT_2:def 1; :: thesis: verum