let n be non zero Nat; :: thesis: for f being NtoSEG Function of (Segm 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 (Segm 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 A1: i in Segm n by NAT_1:44;
then consider ii being Element of Segm n such that
A2: ii = i ;
A3: ntoSeg ii = succ (Segm ii)
.= Segm (ii + 1) by NAT_1:38 ;
thus f . i = i + 1 by Def5, A2, A3; :: thesis: i in dom f
thus i in dom f by A1, FUNCT_2:def 1; :: thesis: verum