let a be real number ; :: thesis: Proj |[a]|,1 = a
reconsider y = a as Real by XREAL_0:def 1;
thus Proj |[a]|,1 = <*y*> /. 1 by JORDAN2B:def 1
.= a by FINSEQ_4:25 ; :: thesis: verum