let p be FinSequence of REAL ; :: thesis: ( p = |[0,0,0]| implies F2M p = <*<*0*>,<*0*>,<*0*>*> )
assume p = |[0,0,0]| ; :: thesis: F2M p = <*<*0*>,<*0*>,<*0*>*>
then ( len p = 3 & p . 1 = 0 & p . 2 = 0 & p . 3 = 0 ) by FINSEQ_1:45;
hence F2M p = <*<*0*>,<*0*>,<*0*>*> by DEF1; :: thesis: verum