deffunc H₁( Nat) -> set = $1 |^ n;
let e1, e2 be FinSequence of REAL ; :: thesis: ( dom e1 = Seg k & ( for i being Nat st i in dom e1 holds
e1 . i = i |^ n ) & dom e2 = Seg k & ( for i being Nat st i in dom e2 holds
e2 . i = i |^ n ) implies e1 = e2 )
assume that
A3: ( dom e1 = Seg k & ( for i being Nat st i in dom e1 holds
e1 . i = H₁(i) ) ) and
A4: ( dom e2 = Seg k & ( for i being Nat st i in dom e2 holds
e2 . i = H₁(i) ) ) ; :: thesis: e1 = e2
for i being Nat st i in dom e1 holds
e1 . i = e2 . i

proof

let i be Nat; :: thesis: ( i in dom e1 implies e1 . i = e2 . i )
assume A5: i in dom e1 ; :: thesis: e1 . i = e2 . i
hence e1 . i = H₁(i) by A3
.= e2 . i by A5, A3, A4 ;
:: thesis: verum

end;

hence e1 = e2 by A3, A4, FINSEQ_1:13; :: thesis: verum