reconsider H = {[2,(FIB . 2)]} as Function ;
A1: dom H = {2} by RELAT_1:9;
dom H c= Seg 2
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom H or x in Seg 2 )
assume x in dom H ; :: thesis: x in Seg 2
then x = 2 by A1, TARSKI:def 1;
hence x in Seg 2 ; :: thesis: verum
end;
then reconsider H = H as FinSubsequence by FINSEQ_1:def 12;
2 in NAT ;
then 2 in dom FIB by FUNCT_2:def 1;
then Seq (FIB | {2}) = Seq H by GRFUNC_1:28
.= <*(FIB . 2)*> by FINSEQ_3:157
.= <*1*> by Def2, Th21 ;
hence Seq (FIB | {2}) = <*1*> ; :: thesis: verum