deffunc H₁( Nat) -> set = (($1 - 1) * ((n + 1) - $1)) + 1;
consider FS being FinSequence such that
A1: ( len FS = n + 1 & ( for i being Nat st i in dom FS holds
FS . i = H₁(i) ) ) from FINSEQ_1:sch 2();
take FS ; :: thesis: ( dom FS = Seg (n + 1) & ( for i being Nat st i in dom FS holds
FS . i = ((i - 1) * ((n + 1) - i)) + 1 ) )
thus ( dom FS = Seg (n + 1) & ( for i being Nat st i in dom FS holds
FS . i = ((i - 1) * ((n + 1) - i)) + 1 ) ) by A1, FINSEQ_1:def 3; :: thesis: verum