let D be non empty set ; :: thesis: for p being FinSequence of D st len p = 3 holds
<*p*> @ = F2M p
let p be FinSequence of D; :: thesis: ( len p = 3 implies <*p*> @ = F2M p )
assume A1: len p = 3 ; :: thesis: <*p*> @ = F2M p
then <*p*> @ = <*<*(p . 1)*>,<*(p . 2)*>,<*(p . 3)*>*> by Th63;
hence <*p*> @ = F2M p by A1, DEF1; :: thesis: verum