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