reconsider f = 2 |-> 1 as FinSequence of REAL by FINSEQ_2:77;
thus 1.REAL 2 = 1* 2 by JORDAN2C:def 8
.= f by JORDAN2C:def 7
.= <*1,1*> by FINSEQ_2:75 ; :: thesis: verum