let D be non empty set ; 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; ( len pf = 3 implies <*(Col (<*pf*>,1)),(Col (<*pf*>,2)),(Col (<*pf*>,3))*> = F2M pf )
assume A0:
len pf = 3
; <*(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; verum