let D be non empty set ; :: thesis: for pf being FinSequence of D st len pf = 3 holds
<*(Col (<*pf*>,1)),(Col (<*pf*>,2)),(Col (<*pf*>,3))*> = F2M pf
let pf be FinSequence of D; :: thesis: ( len pf = 3 implies <*(Col (<*pf*>,1)),(Col (<*pf*>,2)),(Col (<*pf*>,3))*> = F2M pf )
assume A0: len pf = 3 ; :: thesis: <*(Col (<*pf*>,1)),(Col (<*pf*>,2)),(Col (<*pf*>,3))*> = F2M pf
then ( Col (<*pf*>,1) = <*(pf . 1)*> & Col (<*pf*>,2) = <*(pf . 2)*> & Col (<*pf*>,3) = <*(pf . 3)*> ) by Th51;
hence <*(Col (<*pf*>,1)),(Col (<*pf*>,2)),(Col (<*pf*>,3))*> = F2M pf by A0, DEF1; :: thesis: verum